src/HOL/Nominal/nominal_inductive.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30435 e62d6ecab6ad
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4      val atomTs = distinct op = (maps (map snd o #2) prems);
     1.5      val ind_sort = if null atomTs then HOLogic.typeS
     1.6        else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
     1.7 -        ("fs_" ^ NameSpace.base_name (fst (dest_Type T)))) atomTs);
     1.8 +        ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs);
     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 @@ -273,7 +273,7 @@
    1.13  
    1.14      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    1.15      val pt2_atoms = map (fn aT => PureThy.get_thm thy
    1.16 -      ("pt_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    1.17 +      ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    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 @@ -281,7 +281,7 @@
    1.22      val fresh_bij = PureThy.get_thms thy "fresh_bij";
    1.23      val perm_bij = PureThy.get_thms thy "perm_bij";
    1.24      val fs_atoms = map (fn aT => PureThy.get_thm thy
    1.25 -      ("fs_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
    1.26 +      ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
    1.27      val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
    1.28      val fresh_atm = PureThy.get_thms thy "fresh_atm";
    1.29      val swap_simps = PureThy.get_thms thy "swap_simps";
    1.30 @@ -545,7 +545,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
    1.39 @@ -575,7 +575,7 @@
    1.40               Attrib.internal (K (RuleCases.consumes 1))]),
    1.41             strong_inducts) |> snd |>
    1.42          LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
    1.43 -            ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "strong_cases"),
    1.44 +            ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
    1.45                [Attrib.internal (K (RuleCases.case_names (map snd cases))),
    1.46                 Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
    1.47            (strong_cases ~~ induct_cases')) |> snd
    1.48 @@ -665,7 +665,7 @@
    1.49    in
    1.50      ctxt |>
    1.51      LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
    1.52 -        ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "eqvt"),
    1.53 +        ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
    1.54            [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
    1.55        (names ~~ transp thss)) |> snd
    1.56    end;