changeset 19897 | fe661eb3b0e7 |
parent 19884 | a7be206d8655 |
child 19953 | 2f54a51f1801 |
--- a/src/Pure/Tools/codegen_theorems.ML Thu Jun 15 18:35:16 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Thu Jun 15 23:08:54 2006 +0200 @@ -604,7 +604,7 @@ | _ => raise ERROR "rewrite_rhs") | _ => raise ERROR "rewrite_rhs"); fun unvarify thms = - #1 (ProofContext.import true thms (ProofContext.init thy)); + #1 (Variable.import true thms (ProofContext.init thy)); val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy)); in thms