src/HOL/Tools/typedef_package.ML
changeset 12338 de0f4a63baa5
parent 12043 8c86683597a8
child 12624 9ed65232429c
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4      val full = Sign.full_name (Theory.sign_of thy);
     1.5  
     1.6      fun arity_of (raw_name, args, mx) =
     1.7 -      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
     1.8 +      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
     1.9    in
    1.10      if can (Theory.assert_super HOL.thy) thy then
    1.11        thy
    1.12 @@ -97,7 +97,7 @@
    1.13  (* prepare_typedef *)
    1.14  
    1.15  fun read_term sg used s =
    1.16 -  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT));
    1.17 +  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.typeT));
    1.18  
    1.19  fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
    1.20  
    1.21 @@ -125,7 +125,7 @@
    1.22      val goal_pat = mk_nonempty (Var (vname, setT));
    1.23  
    1.24      (*lhs*)
    1.25 -    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
    1.26 +    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.typeS)) vs;
    1.27      val tname = Syntax.type_name t mx;
    1.28      val full_tname = full tname;
    1.29      val newT = Type (full_tname, map TFree lhs_tfrees);
    1.30 @@ -162,7 +162,9 @@
    1.31            fun make th = Drule.standard (th OF [type_definition]);
    1.32            val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
    1.33                Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
    1.34 -            theory' |> PureThy.add_thms
    1.35 +            theory'
    1.36 +            |> Theory.add_path name
    1.37 +            |> PureThy.add_thms
    1.38                ([((Rep_name, make Rep), []),
    1.39                  ((Rep_name ^ "_inverse", make Rep_inverse), []),
    1.40                  ((Abs_name ^ "_inverse", make Abs_inverse), []),
    1.41 @@ -175,7 +177,8 @@
    1.42                  ((Rep_name ^ "_induct", make Rep_induct),
    1.43                    [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
    1.44                  ((Abs_name ^ "_induct", make Abs_induct),
    1.45 -                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]);
    1.46 +                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
    1.47 +            |>> Theory.parent_path;
    1.48            val result = {type_definition = type_definition, set_def = set_def,
    1.49              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
    1.50              Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,