equal
deleted
inserted
replaced
134 |> Theory.absolute_path |
134 |> Theory.absolute_path |
135 |> PureThy.store_thm |
135 |> PureThy.store_thm |
136 ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), []) |
136 ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), []) |
137 ||> Theory.restore_naming thy; |
137 ||> Theory.restore_naming thy; |
138 |
138 |
139 val ivs = Drule.vars_of_terms |
139 val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []); |
140 [Logic.varify (DatatypeProp.make_ind [descr] sorts)]; |
140 val rvs = rev (Drule.fold_terms Term.add_vars thm' []); |
141 val rvs = Drule.vars_of_terms [prop_of thm']; |
|
142 val ivs1 = map Var (filter_out (fn (_, T) => |
141 val ivs1 = map Var (filter_out (fn (_, T) => |
143 tname_of (body_type T) mem ["set", "bool"]) ivs); |
142 tname_of (body_type T) mem ["set", "bool"]) ivs); |
144 val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs; |
143 val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs; |
145 |
144 |
146 val prf = foldr forall_intr_prf |
145 val prf = foldr forall_intr_prf |