| changeset 59633 | a372513af1e2 |
| parent 59621 | 291934bac95e |
| child 63156 | 3cb84e4469a7 |
--- a/src/Tools/Code/code_simp.ML Fri Mar 06 23:44:57 2015 +0100 +++ b/src/Tools/Code/code_simp.ML Fri Mar 06 23:52:14 2015 +0100 @@ -83,7 +83,7 @@ THEN' conclude_tac ctxt NONE ctxt; fun dynamic_value ctxt = - snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.global_cterm_of (Proof_Context.theory_of ctxt); + snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of ctxt; val _ = Theory.setup (Method.setup @{binding code_simp}