equal
deleted
inserted
replaced
139 Goal.prove lthy [] [] prop (K tac) |
139 Goal.prove lthy [] [] prop (K tac) |
140 end |
140 end |
141 |
141 |
142 fun one_def (Free(n,_)) r = |
142 fun one_def (Free(n,_)) r = |
143 let val b = Long_Name.base_name n |
143 let val b = Long_Name.base_name n |
144 in ((Binding.name (b^"_def"), []), r) end |
144 in ((Binding.name (Thm.def_name b), []), r) end |
145 | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form" |
145 | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form" |
146 fun defs [] _ = [] |
146 fun defs [] _ = [] |
147 | defs (l::[]) r = [one_def l r] |
147 | defs (l::[]) r = [one_def l r] |
148 | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r) |
148 | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r) |
149 val fixdefs = defs lhss fixpoint |
149 val fixdefs = defs lhss fixpoint |