--- a/src/HOL/Tools/inductive_package.ML Wed Jan 05 11:50:55 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML Wed Jan 05 11:56:04 2000 +0100
@@ -777,7 +777,7 @@
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
let
val sign = Theory.sign_of thy;
- val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termTVar) c_strings;
+ val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
val atts = map (Attrib.global_attribute thy) srcs;
val intr_names = map (fst o fst) intro_srcs;