equal
deleted
inserted
replaced
17 ML {* set show_sorts *} |
17 ML {* set show_sorts *} |
18 |
18 |
19 ML {* |
19 ML {* |
20 fun check_thm name = let |
20 fun check_thm name = let |
21 val thy = the_context (); |
21 val thy = the_context (); |
22 val thm = get_thm thy (Facts.Named (name, NONE)); |
22 val thm = PureThy.get_thm thy name; |
23 val {prop, hyps, ...} = rep_thm thm; |
23 val {prop, hyps, ...} = rep_thm thm; |
24 val prems = Logic.strip_imp_prems prop; |
24 val prems = Logic.strip_imp_prems prop; |
25 val _ = if null hyps then () |
25 val _ = if null hyps then () |
26 else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^ |
26 else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^ |
27 "Consistency check of locales package failed."); |
27 "Consistency check of locales package failed."); |