equal
deleted
inserted
replaced
142 |
142 |
143 val (vmap, prop_thawed) = Type.varify [] prop |
143 val (vmap, prop_thawed) = Type.varify [] prop |
144 val thawed_prop_consts = collect_consts (prop_thawed,[]) |
144 val thawed_prop_consts = collect_consts (prop_thawed,[]) |
145 val (altcos,overloaded) = Library.split_list cos |
145 val (altcos,overloaded) = Library.split_list cos |
146 val (names,sconsts) = Library.split_list altcos |
146 val (names,sconsts) = Library.split_list altcos |
147 val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts |
147 val consts = map (term_of o Thm.read_cterm thy o rpair dummyT) sconsts |
148 val _ = not (Library.exists (not o Term.is_Const) consts) |
148 val _ = not (Library.exists (not o Term.is_Const) consts) |
149 orelse error "Specification: Non-constant found as parameter" |
149 orelse error "Specification: Non-constant found as parameter" |
150 |
150 |
151 fun proc_const c = |
151 fun proc_const c = |
152 let |
152 let |