src/HOL/Tools/inductive_realizer.ML
changeset 30364 577edc39b501
parent 30345 76fd85bbf139
child 30435 e62d6ecab6ad
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -68,8 +68,8 @@
     1.4      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
     1.5        (Logic.strip_imp_concl (prop_of (hd intrs))));
     1.6      val params = map dest_Var (Library.take (nparms, ts));
     1.7 -    val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs));
     1.8 -    fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)),
     1.9 +    val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
    1.10 +    fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
    1.11        map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
    1.12          filter_out (equal Extraction.nullT) (map
    1.13            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    1.14 @@ -112,7 +112,7 @@
    1.15      val rT = if n then Extraction.nullT
    1.16        else Type (space_implode "_" (s ^ "T" :: vs),
    1.17          map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
    1.18 -    val r = if n then Extraction.nullt else Var ((NameSpace.base_name s, 0), rT);
    1.19 +    val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
    1.20      val S = list_comb (h, params @ xs);
    1.21      val rvs = relevant_vars S;
    1.22      val vs' = map fst rvs \\ vs;
    1.23 @@ -195,7 +195,7 @@
    1.24            in if conclT = Extraction.nullT
    1.25              then list_abs_free (map dest_Free xs, HOLogic.unit)
    1.26              else list_abs_free (map dest_Free xs, list_comb
    1.27 -              (Free ("r" ^ NameSpace.base_name (name_of_thm intr),
    1.28 +              (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
    1.29                  map fastype_of (rev args) ---> conclT), rev args))
    1.30            end
    1.31  
    1.32 @@ -217,7 +217,7 @@
    1.33        end) (premss ~~ dummies);
    1.34      val frees = fold Term.add_frees fs [];
    1.35      val Ts = map fastype_of fs;
    1.36 -    fun name_of_fn intr = "r" ^ NameSpace.base_name (name_of_thm intr)
    1.37 +    fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr)
    1.38    in
    1.39      fst (fold_map (fn concl => fn names =>
    1.40        let val T = Extraction.etype_of thy vs [] concl
    1.41 @@ -245,7 +245,7 @@
    1.42        |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
    1.43      handle DatatypeAux.Datatype_Empty name' =>
    1.44        let
    1.45 -        val name = NameSpace.base_name name';
    1.46 +        val name = Long_Name.base_name name';
    1.47          val dname = Name.variant used "Dummy";
    1.48        in
    1.49          thy
    1.50 @@ -273,8 +273,8 @@
    1.51  
    1.52  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
    1.53    let
    1.54 -    val qualifier = NameSpace.qualifier (name_of_thm induct);
    1.55 -    val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
    1.56 +    val qualifier = Long_Name.qualifier (name_of_thm induct);
    1.57 +    val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
    1.58      val iTs = OldTerm.term_tvars (prop_of (hd intrs));
    1.59      val ar = length vs + length iTs;
    1.60      val params = InductivePackage.params_of raw_induct;
    1.61 @@ -285,18 +285,18 @@
    1.62      val rss' = map (fn (((s, rs), (_, arity)), elim) =>
    1.63        (s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs)))
    1.64          (rss ~~ arities ~~ elims);
    1.65 -    val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
    1.66 +    val (prfx, _) = split_last (Long_Name.explode (fst (hd rss)));
    1.67      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
    1.68  
    1.69      val thy1 = thy |>
    1.70        Sign.root_path |>
    1.71 -      Sign.add_path (NameSpace.implode prfx);
    1.72 +      Sign.add_path (Long_Name.implode prfx);
    1.73      val (ty_eqs, rlz_eqs) = split_list
    1.74        (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
    1.75  
    1.76      val thy1' = thy1 |>
    1.77        Theory.copy |>
    1.78 -      Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |>
    1.79 +      Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
    1.80        fold (fn s => AxClass.axiomatize_arity
    1.81          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
    1.82          Extraction.add_typeof_eqns_i ty_eqs;
    1.83 @@ -334,7 +334,7 @@
    1.84        rintrs |> map (fn rintr =>
    1.85          let
    1.86            val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
    1.87 -          val s' = NameSpace.base_name s;
    1.88 +          val s' = Long_Name.base_name s;
    1.89            val T' = Logic.unvarifyT T;
    1.90          in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
    1.91        |> distinct (op = o pairself (#1 o #1))
    1.92 @@ -352,7 +352,7 @@
    1.93          {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
    1.94            coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    1.95          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.96 -          ((Binding.name (NameSpace.base_name (name_of_thm intr)), []),
    1.97 +          ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
    1.98             subst_atomic rlzpreds' (Logic.unvarify rintr)))
    1.99               (rintrs ~~ maps snd rss)) [] ||>
   1.100        Sign.absolute_path;
   1.101 @@ -395,12 +395,12 @@
   1.102               [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
   1.103                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   1.104          val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
   1.105 -          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
   1.106 +          (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
   1.107          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
   1.108            (DatatypeAux.split_conj_thm thm');
   1.109          val ([thms'], thy'') = PureThy.add_thmss
   1.110            [((Binding.name (space_implode "_"
   1.111 -             (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
   1.112 +             (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
   1.113                 ["correctness"])), thms), [])] thy';
   1.114          val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
   1.115        in
   1.116 @@ -409,7 +409,7 @@
   1.117                mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
   1.118              realizers @ (case realizers of
   1.119               [(((ind, corr), rlz), r)] =>
   1.120 -               [mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct",
   1.121 +               [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
   1.122                    ind, corr, rlz, r)]
   1.123             | _ => [])) thy''
   1.124        end;