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 (* FIXME better avoid this low-level stuff *) |
|
58 fun inferT sg pre_tm = |
|
59 let |
|
60 val pp = Sign.pp sg; |
|
61 val consts = Sign.consts_of sg; |
|
62 val (t, _) = |
|
63 Sign.infer_types pp sg consts (K NONE) (K NONE) Name.context true |
|
64 ([pre_tm],propT); |
|
65 in t end; |
|
66 |
|
67 fun pg'' thy defs t tacs = |
57 fun pg'' thy defs t tacs = |
68 let |
58 let |
69 val t' = inferT thy t; |
59 val t' = FixrecPackage.legacy_infer_term thy t; |
70 val asms = Logic.strip_imp_prems t'; |
60 val asms = Logic.strip_imp_prems t'; |
71 val prop = Logic.strip_imp_concl t'; |
61 val prop = Logic.strip_imp_concl t'; |
72 fun tac prems = |
62 fun tac prems = |
73 rewrite_goals_tac defs THEN |
63 rewrite_goals_tac defs THEN |
74 EVERY (tacs (map (rewrite_rule defs) prems)); |
64 EVERY (tacs (map (rewrite_rule defs) prems)); |