adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

apply_trace: avoid conjunctionI before tracing

This commit is contained in:
Daniel Matichuk 2016-04-19 14:52:24 +10:00
parent 65e48e236b
commit d543517bb1
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Apply_Trace.thy
View File

@ -71,7 +71,7 @@ fun proof_body_descend' (_,("",_,body)) = fold (append o proof_body_descend') (t
fun used_facts thm = fold (append o proof_body_descend') (thms_of (Thm.proof_body_of thm)) []
fun raw_primitive_text f = Method.Basic (fn _ => (Method.METHOD (K (fn thm => Seq.single (f thm)))))
fun raw_primitive_text f = Method.Basic (fn _ => ((K (fn (ctxt, thm) => Seq.make_results (Seq.single (ctxt, f thm))))))
(*Find local facts from new hyps*)