equal
deleted
inserted
replaced
15 |
15 |
16 structure LocalDefs: LOCAL_DEFS = |
16 structure LocalDefs: LOCAL_DEFS = |
17 struct |
17 struct |
18 |
18 |
19 |
19 |
20 val refl_tac = Tactic.rtac Drule.reflexive_thm; |
20 val refl_tac = Tactic.rtac (standard (Drule.reflexive_thm RS Drule.triv_goal)); |
21 |
21 |
22 |
22 |
23 fun gen_def fix prep_term match_binds name atts ((x, raw_T), (raw_rhs, raw_pats)) state = |
23 fun gen_def fix prep_term match_binds name atts ((x, raw_T), (raw_rhs, raw_pats)) state = |
24 let |
24 let |
25 fun err msg = raise Proof.STATE ("Bad local def: " ^ msg, state); |
25 fun err msg = raise Proof.STATE ("Bad local def: " ^ msg, state); |