src/HOL/Nominal/nominal_inductive2.ML
changeset 30364 577edc39b501
parent 30307 6c74ef5a349f
child 30450 7655e6533209
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -229,7 +229,7 @@
     1.4      val atoms = map (fst o dest_Type) atomTs;
     1.5      val ind_sort = if null atomTs then HOLogic.typeS
     1.6        else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
     1.7 -        ("fs_" ^ NameSpace.base_name a)) atoms);
     1.8 +        ("fs_" ^ Long_Name.base_name a)) atoms);
     1.9      val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
    1.10      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    1.11      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    1.12 @@ -296,7 +296,7 @@
    1.13  
    1.14      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    1.15      val pt2_atoms = map (fn a => PureThy.get_thm thy
    1.16 -      ("pt_" ^ NameSpace.base_name a ^ "2")) atoms;
    1.17 +      ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
    1.18      val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
    1.19        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    1.20        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    1.21 @@ -324,7 +324,7 @@
    1.22          val atom = fst (dest_Type T);
    1.23          val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
    1.24          val fs_atom = PureThy.get_thm thy
    1.25 -          ("fs_" ^ NameSpace.base_name atom ^ "1");
    1.26 +          ("fs_" ^ Long_Name.base_name atom ^ "1");
    1.27          val avoid_th = Drule.instantiate'
    1.28            [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
    1.29            ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
    1.30 @@ -452,7 +452,7 @@
    1.31      ctxt'' |>
    1.32      Proof.theorem_i NONE (fn thss => fn ctxt =>
    1.33        let
    1.34 -        val rec_name = space_implode "_" (map NameSpace.base_name names);
    1.35 +        val rec_name = space_implode "_" (map Long_Name.base_name names);
    1.36          val rec_qualified = Binding.qualify false rec_name;
    1.37          val ind_case_names = RuleCases.case_names induct_cases;
    1.38          val induct_cases' = InductivePackage.partition_rules' raw_induct