changeset 35845 | e5980f0ad025 |
parent 35669 | a91c7ed801b8 |
child 36460 | c643b23e8592 |
child 36463 | 3793f1c83046 |
--- a/src/Pure/Isar/class.ML Sat Mar 20 02:23:41 2010 +0100 +++ b/src/Pure/Isar/class.ML Sat Mar 20 17:33:11 2010 +0100 @@ -257,7 +257,7 @@ | t => t); val raw_pred = Locale.intros_of thy class |> fst - |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of); + |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); fun get_axiom thy = case (#axioms o AxClass.get_info thy) class of [] => NONE | [thm] => SOME thm;