src/HOL/Tools/typedef_package.ML

 fun add_typedecls decls thy =
   let
     val full = Sign.full_name (Theory.sign_of thy);
 
     fun arity_of (raw_name, args, mx) =
-      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
+      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
   in
     if can (Theory.assert_super HOL.thy) thy then
       thy
       |> PureThy.add_typedecls decls
       |> Theory.add_arities_i (map arity_of decls)

 
 
 (* prepare_typedef *)
 
 fun read_term sg used s =
-  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT));
+  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.typeT));
 
 fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
 
 fun err_in_typedef name =
   error ("The error(s) above occurred in typedef " ^ quote name);

     val vname = take_suffix Symbol.is_digit (Symbol.explode name)
       |> apfst implode |> apsnd (#1 o Term.read_int);
     val goal_pat = mk_nonempty (Var (vname, setT));
 
     (*lhs*)
-    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
+    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.typeS)) vs;
     val tname = Syntax.type_name t mx;
     val full_tname = full tname;
     val newT = Type (full_tname, map TFree lhs_tfrees);
 
     val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);

       |> (fn ((theory', [type_definition]), set_def) =>
         let
           fun make th = Drule.standard (th OF [type_definition]);
           val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
               Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
-            theory' |> PureThy.add_thms
+            theory'
+            |> Theory.add_path name
+            |> PureThy.add_thms
               ([((Rep_name, make Rep), []),
                 ((Rep_name ^ "_inverse", make Rep_inverse), []),
                 ((Abs_name ^ "_inverse", make Abs_inverse), []),
                 ((Rep_name ^ "_inject", make Rep_inject), []),
                 ((Abs_name ^ "_inject", make Abs_inject), []),

                 ((Abs_name ^ "_cases", make Abs_cases),
                   [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
                 ((Rep_name ^ "_induct", make Rep_induct),
                   [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
                 ((Abs_name ^ "_induct", make Abs_induct),
-                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]);
+                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
+            |>> Theory.parent_path;
           val result = {type_definition = type_definition, set_def = set_def,
             Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
             Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
             Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
         in ((theory'', type_definition), result) end);