equal
deleted
inserted
replaced
52 infix 9 `%%; |
52 infix 9 `%%; |
53 infixr 9 oo; |
53 infixr 9 oo; |
54 |
54 |
55 (* ----- general proof facilities ------------------------------------------- *) |
55 (* ----- general proof facilities ------------------------------------------- *) |
56 |
56 |
|
57 fun legacy_infer_term thy t = |
|
58 let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy) |
|
59 in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end; |
|
60 |
57 fun pg'' thy defs t tacs = |
61 fun pg'' thy defs t tacs = |
58 let |
62 let |
59 val t' = FixrecPackage.legacy_infer_term thy t; |
63 val t' = legacy_infer_term thy t; |
60 val asms = Logic.strip_imp_prems t'; |
64 val asms = Logic.strip_imp_prems t'; |
61 val prop = Logic.strip_imp_concl t'; |
65 val prop = Logic.strip_imp_concl t'; |
62 fun tac prems = |
66 fun tac prems = |
63 rewrite_goals_tac defs THEN |
67 rewrite_goals_tac defs THEN |
64 EVERY (tacs (map (rewrite_rule defs) prems)); |
68 EVERY (tacs (map (rewrite_rule defs) prems)); |