src/HOL/Tools/inductive_package.ML
changeset 8100 6186ee807f2e
parent 7798 42e94b618f34
child 8277 493707fcd8a6
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jan 05 11:50:55 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jan 05 11:56:04 2000 +0100
     1.3 @@ -777,7 +777,7 @@
     1.4  fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
     1.5    let
     1.6      val sign = Theory.sign_of thy;
     1.7 -    val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termTVar) c_strings;
     1.8 +    val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
     1.9  
    1.10      val atts = map (Attrib.global_attribute thy) srcs;
    1.11      val intr_names = map (fst o fst) intro_srcs;