replaced Term.variant(list) by Name.variant(_list);
authorwenzelm
Tue Jul 11 12:16:54 2006 +0200 (2006-07-11)
changeset 200718f3e1ddb50e6
parent 20070 3f31fb81b83a
child 20072 c4710df2c953
replaced Term.variant(list) by Name.variant(_list);
TFL/rules.ML
TFL/usyntax.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/EfficientNat.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/split_rule.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/fixrec_package.ML
src/Provers/IsaPlanner/isand.ML
src/Provers/IsaPlanner/rw_inst.ML
src/Provers/eqsubst.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Tools/codegen_thingol.ML
src/Pure/codegen.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/thm.ML
src/Pure/type.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/TFL/rules.ML	Tue Jul 11 12:16:52 2006 +0200
     1.2 +++ b/TFL/rules.ML	Tue Jul 11 12:16:54 2006 +0200
     1.3 @@ -513,8 +513,8 @@
     1.4              let val eq = Logic.strip_imp_concl body
     1.5                  val (f,args) = S.strip_comb (get_lhs eq)
     1.6                  val (vstrl,_) = S.strip_abs f
     1.7 -                val names  = variantlist (map (#1 o dest_Free) vstrl,
     1.8 -                                          add_term_names(body, []))
     1.9 +                val names  =
    1.10 +                  Name.variant_list (add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
    1.11              in get (rst, n+1, (names,n)::L) end
    1.12              handle TERM _ => get (rst, n+1, L)
    1.13                | U.ERR _ => get (rst, n+1, L);
     2.1 --- a/TFL/usyntax.ML	Tue Jul 11 12:16:52 2006 +0200
     2.2 +++ b/TFL/usyntax.ML	Tue Jul 11 12:16:54 2006 +0200
     2.3 @@ -240,7 +240,7 @@
     2.4  
     2.5  fun dest_abs used (a as Abs(s, ty, M)) =
     2.6       let
     2.7 -       val s' = variant used s;
     2.8 +       val s' = Name.variant used s;
     2.9         val v = Free(s', ty);
    2.10       in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
    2.11       end
     3.1 --- a/src/HOL/Import/hol4rews.ML	Tue Jul 11 12:16:52 2006 +0200
     3.2 +++ b/src/HOL/Import/hol4rews.ML	Tue Jul 11 12:16:54 2006 +0200
     3.3 @@ -735,7 +735,7 @@
     3.4  		then F defname                 (* name_def *)
     3.5  		else if not (pdefname mem used)
     3.6  		then F pdefname                (* name_primdef *)
     3.7 -		else F (variant used pdefname) (* last resort *)
     3.8 +		else F (Name.variant used pdefname) (* last resort *)
     3.9  	    end
    3.10      end
    3.11  
     4.1 --- a/src/HOL/Import/shuffler.ML	Tue Jul 11 12:16:52 2006 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Tue Jul 11 12:16:54 2006 +0200
     4.3 @@ -253,7 +253,7 @@
     4.4  	val (type_inst,_) =
     4.5  	    Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
     4.6  		      let
     4.7 -			  val v' = variant used v
     4.8 +			  val v' = Name.variant used v
     4.9  		      in
    4.10  			  ((w,TFree(v',S))::inst,v'::used)
    4.11  		      end)
    4.12 @@ -322,7 +322,7 @@
    4.13  	      then
    4.14  		  let
    4.15  		      val cert = cterm_of sg
    4.16 -		      val v = Free(variant (add_term_free_names(t,[])) "v",xT)
    4.17 +		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
    4.18  		      val cv = cert v
    4.19  		      val ct = cert t
    4.20  		      val th = (assume ct)
    4.21 @@ -385,7 +385,7 @@
    4.22  		      Type("fun",[aT,bT]) =>
    4.23  		      let
    4.24  			  val cert = cterm_of sg
    4.25 -			  val vname = variant (add_term_free_names(t,[])) "v"
    4.26 +			  val vname = Name.variant (add_term_free_names(t,[])) "v"
    4.27  			  val v = Free(vname,aT)
    4.28  			  val cv = cert v
    4.29  			  val ct = cert t
     5.1 --- a/src/HOL/Library/EfficientNat.thy	Tue Jul 11 12:16:52 2006 +0200
     5.2 +++ b/src/HOL/Library/EfficientNat.thy	Tue Jul 11 12:16:54 2006 +0200
     5.3 @@ -153,7 +153,7 @@
     5.4  fun remove_suc thy thms =
     5.5    let
     5.6      val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
     5.7 -    val vname = variant (map fst
     5.8 +    val vname = Name.variant (map fst
     5.9        (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
    5.10      val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
    5.11      fun lhs_of th = snd (Thm.dest_comb
    5.12 @@ -206,7 +206,7 @@
    5.13  fun remove_suc_clause thy thms =
    5.14    let
    5.15      val Suc_clause' = Thm.transfer thy Suc_clause;
    5.16 -    val vname = variant (map fst
    5.17 +    val vname = Name.variant (map fst
    5.18        (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
    5.19      fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
    5.20        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
     6.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jul 11 12:16:52 2006 +0200
     6.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jul 11 12:16:54 2006 +0200
     6.3 @@ -252,7 +252,7 @@
     6.4    let val used = add_term_names (t, [])
     6.5            and vars = term_vars t;
     6.6        fun newName (Var(ix,_), (pairs,used)) = 
     6.7 -          let val v = variant used (string_of_indexname ix)
     6.8 +          let val v = Name.variant used (string_of_indexname ix)
     6.9            in  ((ix,v)::pairs, v::used)  end;
    6.10        val (alist, _) = foldr newName ([], used) vars;
    6.11        fun mk_inst (Var(v,T)) = (Var(v,T),
     7.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Jul 11 12:16:52 2006 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Jul 11 12:16:54 2006 +0200
     7.3 @@ -553,7 +553,7 @@
     7.4                QUIET_BREADTH_FIRST (has_fewer_prems 1)
     7.5                (resolve_tac rep_intrs 1))) thy |> (fn (r, thy) =>
     7.6          let
     7.7 -          val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
     7.8 +          val permT = mk_permT (TFree (Name.variant tvs "'a", HOLogic.typeS));
     7.9            val pi = Free ("pi", permT);
    7.10            val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
    7.11            val T = Type (Sign.intern_type thy name, tvs');
    7.12 @@ -1096,11 +1096,11 @@
    7.13          val recs = List.filter is_rec_type cargs;
    7.14          val Ts = map (typ_of_dtyp descr'' sorts') cargs;
    7.15          val recTs' = map (typ_of_dtyp descr'' sorts') recs;
    7.16 -        val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
    7.17 +        val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
    7.18          val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
    7.19          val frees = tnames ~~ Ts;
    7.20          val frees' = partition_cargs idxs frees;
    7.21 -        val z = (variant tnames "z", fsT);
    7.22 +        val z = (Name.variant tnames "z", fsT);
    7.23  
    7.24          fun mk_prem ((dt, s), T) =
    7.25            let
    7.26 @@ -1126,7 +1126,7 @@
    7.27          Const ("Nominal.fresh", T --> fsT --> HOLogic.boolT) $ t $ u) i T)
    7.28            (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
    7.29      val tnames = DatatypeProp.make_tnames recTs;
    7.30 -    val zs = variantlist (replicate (length descr'') "z", tnames);
    7.31 +    val zs = Name.variant_list tnames (replicate (length descr'') "z");
    7.32      val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
    7.33        (map (fn ((((i, _), T), tname), z) =>
    7.34          make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
     8.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jul 11 12:16:52 2006 +0200
     8.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jul 11 12:16:54 2006 +0200
     8.3 @@ -280,7 +280,7 @@
     8.4      val recTs = get_rec_types descr' sorts;
     8.5      val used = foldr add_typ_tfree_names [] recTs;
     8.6      val newTs = Library.take (length (hd descr), recTs);
     8.7 -    val T' = TFree (variant used "'t", HOLogic.typeS);
     8.8 +    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
     8.9  
    8.10      fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
    8.11  
     9.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Jul 11 12:16:52 2006 +0200
     9.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jul 11 12:16:54 2006 +0200
     9.3 @@ -219,7 +219,7 @@
     9.4            | pcase gr ((cname, cargs)::cs) (t::ts) (U::Us) =
     9.5                let
     9.6                  val j = length cargs;
     9.7 -                val xs = variantlist (replicate j "x", names);
     9.8 +                val xs = Name.variant_list names (replicate j "x");
     9.9                  val Us' = Library.take (j, fst (strip_type U));
    9.10                  val frees = map Free (xs ~~ Us');
    9.11                  val (gr0, cp) = invoke_codegen thy defs dep module false
    10.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jul 11 12:16:52 2006 +0200
    10.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jul 11 12:16:54 2006 +0200
    10.3 @@ -609,7 +609,7 @@
    10.4      val size_names = DatatypeProp.indexify_names
    10.5        (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)));
    10.6  
    10.7 -    val freeT = TFree (variant used "'t", HOLogic.typeS);
    10.8 +    val freeT = TFree (Name.variant used "'t", HOLogic.typeS);
    10.9      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   10.10        map (fn (_, cargs) =>
   10.11          let val Ts = map (typ_of_dtyp descr' sorts) cargs
    11.1 --- a/src/HOL/Tools/datatype_prop.ML	Tue Jul 11 12:16:52 2006 +0200
    11.2 +++ b/src/HOL/Tools/datatype_prop.ML	Tue Jul 11 12:16:54 2006 +0200
    11.3 @@ -108,7 +108,7 @@
    11.4          val recs = List.filter is_rec_type cargs;
    11.5          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    11.6          val recTs' = map (typ_of_dtyp descr' sorts) recs;
    11.7 -        val tnames = variantlist (make_tnames Ts, pnames);
    11.8 +        val tnames = Name.variant_list pnames (make_tnames Ts);
    11.9          val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   11.10          val frees = tnames ~~ Ts;
   11.11          val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
   11.12 @@ -136,7 +136,7 @@
   11.13      fun make_casedist_prem T (cname, cargs) =
   11.14        let
   11.15          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   11.16 -        val frees = variantlist (make_tnames Ts, ["P", "y"]) ~~ Ts;
   11.17 +        val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
   11.18          val free_ts = map Free frees
   11.19        in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
   11.20          (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
   11.21 @@ -158,7 +158,7 @@
   11.22    let
   11.23      val descr' = List.concat descr;
   11.24  
   11.25 -    val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
   11.26 +    val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~
   11.27        replicate (length descr') HOLogic.typeS);
   11.28  
   11.29      val reccomb_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) =>
   11.30 @@ -234,7 +234,7 @@
   11.31      val recTs = get_rec_types descr' sorts;
   11.32      val used = foldr add_typ_tfree_names [] recTs;
   11.33      val newTs = Library.take (length (hd descr), recTs);
   11.34 -    val T' = TFree (variant used "'t", HOLogic.typeS);
   11.35 +    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   11.36  
   11.37      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   11.38        map (fn (_, cargs) =>
   11.39 @@ -319,7 +319,7 @@
   11.40      val recTs = get_rec_types descr' sorts;
   11.41      val used' = foldr add_typ_tfree_names [] recTs;
   11.42      val newTs = Library.take (length (hd descr), recTs);
   11.43 -    val T' = TFree (variant used' "'t", HOLogic.typeS);
   11.44 +    val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
   11.45      val P = Free ("P", T' --> HOLogic.boolT);
   11.46  
   11.47      fun make_split (((_, (_, _, constrs)), T), comb_t) =
   11.48 @@ -330,7 +330,7 @@
   11.49          fun process_constr (((cname, cargs), f), (t1s, t2s)) =
   11.50            let
   11.51              val Ts = map (typ_of_dtyp descr' sorts) cargs;
   11.52 -            val frees = map Free (variantlist (make_tnames Ts, used) ~~ Ts);
   11.53 +            val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
   11.54              val eqn = HOLogic.mk_eq (Free ("x", T),
   11.55                list_comb (Const (cname, Ts ---> T), frees));
   11.56              val P' = P $ list_comb (f, frees)
   11.57 @@ -437,7 +437,7 @@
   11.58          fun mk_clause ((f, g), (cname, _)) =
   11.59            let
   11.60              val (Ts, _) = strip_type (fastype_of f);
   11.61 -            val tnames = variantlist (make_tnames Ts, used);
   11.62 +            val tnames = Name.variant_list used (make_tnames Ts);
   11.63              val frees = map Free (tnames ~~ Ts)
   11.64            in
   11.65              list_all_free (tnames ~~ Ts, Logic.mk_implies
   11.66 @@ -472,7 +472,7 @@
   11.67      fun mk_eqn T (cname, cargs) =
   11.68        let
   11.69          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   11.70 -        val tnames = variantlist (make_tnames Ts, ["v"]);
   11.71 +        val tnames = Name.variant_list ["v"] (make_tnames Ts);
   11.72          val frees = tnames ~~ Ts
   11.73        in
   11.74          foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
    12.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Jul 11 12:16:52 2006 +0200
    12.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Jul 11 12:16:54 2006 +0200
    12.3 @@ -63,7 +63,7 @@
    12.4        (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) =>
    12.5          let
    12.6            val Ts = map (typ_of_dtyp descr sorts) cargs;
    12.7 -          val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
    12.8 +          val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
    12.9            val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
   12.10            val frees = tnames ~~ Ts;
   12.11  
   12.12 @@ -171,8 +171,7 @@
   12.13      fun make_casedist_prem T (cname, cargs) =
   12.14        let
   12.15          val Ts = map (typ_of_dtyp descr sorts) cargs;
   12.16 -        val frees = variantlist
   12.17 -          (DatatypeProp.make_tnames Ts, ["P", "y"]) ~~ Ts;
   12.18 +        val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
   12.19          val free_ts = map Free frees;
   12.20          val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT)
   12.21        in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
    13.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 11 12:16:52 2006 +0200
    13.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 11 12:16:54 2006 +0200
    13.3 @@ -392,7 +392,7 @@
    13.4          fun mk_thm i =
    13.5            let
    13.6              val Ts = map (TFree o rpair HOLogic.typeS)
    13.7 -              (variantlist (replicate i "'t", used));
    13.8 +              (Name.variant_list used (replicate i "'t"));
    13.9              val f = Free ("f", Ts ---> U)
   13.10            in Goal.prove_global sign [] [] (Logic.mk_implies
   13.11              (HOLogic.mk_Trueprop (HOLogic.list_all
    14.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jul 11 12:16:52 2006 +0200
    14.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jul 11 12:16:54 2006 +0200
    14.3 @@ -2,7 +2,7 @@
    14.4      ID:         $Id$
    14.5      Author:     Alexander Krauss, TU Muenchen
    14.6  
    14.7 -A package for general recursive function definitions. 
    14.8 +A package for general recursive function definitions.
    14.9  Preparation step: makes auxiliary definitions and generates
   14.10  proof obligations.
   14.11  *)
   14.12 @@ -10,20 +10,16 @@
   14.13  signature FUNDEF_PREP =
   14.14  sig
   14.15      val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
   14.16 -			 -> FundefCommon.prep_result * theory
   14.17 +                         -> FundefCommon.prep_result * theory
   14.18  
   14.19  end
   14.20  
   14.21 -
   14.22 -
   14.23 -
   14.24 -
   14.25  structure FundefPrep (*: FUNDEF_PREP*) =
   14.26  struct
   14.27  
   14.28  
   14.29  open FundefCommon
   14.30 -open FundefAbbrev 
   14.31 +open FundefAbbrev
   14.32  
   14.33  (* Theory dependencies. *)
   14.34  val Pair_inject = thm "Product_Type.Pair_inject";
   14.35 @@ -39,30 +35,30 @@
   14.36  
   14.37  
   14.38  fun split_list3 [] = ([],[],[])
   14.39 -  | split_list3 ((x,y,z)::xyzs) = 
   14.40 +  | split_list3 ((x,y,z)::xyzs) =
   14.41      let
   14.42 -	val (xs, ys, zs) = split_list3 xyzs
   14.43 +        val (xs, ys, zs) = split_list3 xyzs
   14.44      in
   14.45 -	(x::xs,y::ys,z::zs)
   14.46 +        (x::xs,y::ys,z::zs)
   14.47      end
   14.48  
   14.49  
   14.50  fun build_tree thy f congs ctx (qs, gs, lhs, rhs) =
   14.51      let
   14.52 -	(* FIXME: Save precomputed dependencies in a theory data slot *)
   14.53 -	val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
   14.54 +        (* FIXME: Save precomputed dependencies in a theory data slot *)
   14.55 +        val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
   14.56  
   14.57 -        val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx 
   14.58 +        val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx
   14.59      in
   14.60 -	FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
   14.61 +        FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
   14.62      end
   14.63  
   14.64  
   14.65  fun find_calls tree =
   14.66      let
   14.67        fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
   14.68 -	| add_Ri _ _ _ _ = raise Match
   14.69 -    in                                 
   14.70 +        | add_Ri _ _ _ _ = raise Match
   14.71 +    in
   14.72        rev (FundefCtxTree.traverse_tree add_Ri tree [])
   14.73      end
   14.74  
   14.75 @@ -71,68 +67,68 @@
   14.76  (* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
   14.77  fun mk_primed_vars thy glrs =
   14.78      let
   14.79 -	val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
   14.80 +        val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
   14.81  
   14.82 -	fun rename_vars (qs,gs,lhs,rhs) =
   14.83 -	    let
   14.84 -		val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
   14.85 -		val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
   14.86 -	    in
   14.87 -		(qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
   14.88 -	    end
   14.89 +        fun rename_vars (qs,gs,lhs,rhs) =
   14.90 +            let
   14.91 +                val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
   14.92 +                val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
   14.93 +            in
   14.94 +                (qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
   14.95 +            end
   14.96      in
   14.97 -	map rename_vars glrs
   14.98 +        map rename_vars glrs
   14.99      end
  14.100  
  14.101  
  14.102  
  14.103  (* Chooses fresh free names, declares G and R, defines f and returns a record
  14.104 -   with all the information *)  
  14.105 +   with all the information *)
  14.106  fun setup_context f glrs defname thy =
  14.107      let
  14.108 -	val Const (f_fullname, fT) = f
  14.109 -	val fname = Sign.base_name f_fullname
  14.110 +        val Const (f_fullname, fT) = f
  14.111 +        val fname = Sign.base_name f_fullname
  14.112  
  14.113 -	val domT = domain_type fT 
  14.114 -	val ranT = range_type fT
  14.115 +        val domT = domain_type fT
  14.116 +        val ranT = range_type fT
  14.117  
  14.118 -	val GT = mk_relT (domT, ranT)
  14.119 -	val RT = mk_relT (domT, domT)
  14.120 -	val G_name = defname ^ "_graph"
  14.121 -	val R_name = defname ^ "_rel"
  14.122 +        val GT = mk_relT (domT, ranT)
  14.123 +        val RT = mk_relT (domT, domT)
  14.124 +        val G_name = defname ^ "_graph"
  14.125 +        val R_name = defname ^ "_rel"
  14.126  
  14.127          val gfixes = [("h_fd", domT --> ranT),
  14.128 -	              ("y_fd", ranT),
  14.129 -	              ("x_fd", domT),
  14.130 -	              ("z_fd", domT),
  14.131 -	              ("a_fd", domT),
  14.132 -	              ("D_fd", HOLogic.mk_setT domT),
  14.133 -	              ("P_fd", domT --> boolT),
  14.134 -	              ("Pb_fd", boolT),
  14.135 -	              ("f_fd", fT)]
  14.136 +                      ("y_fd", ranT),
  14.137 +                      ("x_fd", domT),
  14.138 +                      ("z_fd", domT),
  14.139 +                      ("a_fd", domT),
  14.140 +                      ("D_fd", HOLogic.mk_setT domT),
  14.141 +                      ("P_fd", domT --> boolT),
  14.142 +                      ("Pb_fd", boolT),
  14.143 +                      ("f_fd", fT)]
  14.144  
  14.145          val (fxnames, ctx) = (ProofContext.init thy)
  14.146                                 |> ProofContext.add_fixes_i (map (fn (n,T) => (n, SOME T, NoSyn)) gfixes)
  14.147  
  14.148          val [h, y, x, z, a, D, P, Pbool, fvar] = map (fn (n,(_,T)) => Free (n, T)) (fxnames ~~ gfixes)
  14.149 -                                                                                    
  14.150 +
  14.151          val Free (fvarname, _) = fvar
  14.152  
  14.153 -	val glrs' = mk_primed_vars thy glrs
  14.154 +        val glrs' = mk_primed_vars thy glrs
  14.155  
  14.156 -	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
  14.157 +        val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
  14.158  
  14.159 -	val G = Const (Sign.full_name thy G_name, GT)
  14.160 -	val R = Const (Sign.full_name thy R_name, RT)
  14.161 -	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
  14.162 +        val G = Const (Sign.full_name thy G_name, GT)
  14.163 +        val R = Const (Sign.full_name thy R_name, RT)
  14.164 +        val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
  14.165  
  14.166 -	val f_eq = Logic.mk_equals (f $ x, 
  14.167 -				    Const ("The", (ranT --> boolT) --> ranT) $
  14.168 -					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
  14.169 +        val f_eq = Logic.mk_equals (f $ x,
  14.170 +                                    Const ("The", (ranT --> boolT) --> ranT) $
  14.171 +                                          Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
  14.172  
  14.173 -	val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
  14.174 +        val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
  14.175      in
  14.176 -	(Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy)
  14.177 +        (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy)
  14.178      end
  14.179  
  14.180  
  14.181 @@ -142,8 +138,8 @@
  14.182  (* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
  14.183  fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
  14.184      (implies $ Trueprop (mk_eq (lhs, lhs'))
  14.185 -	     $ Trueprop (mk_eq (rhs, rhs')))
  14.186 -	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
  14.187 +             $ Trueprop (mk_eq (rhs, rhs')))
  14.188 +        |> fold_rev (curry Logic.mk_implies) (gs @ gs')
  14.189          |> fold_rev mk_forall (qs @ qs')
  14.190  
  14.191  (* all proof obligations *)
  14.192 @@ -153,35 +149,35 @@
  14.193  
  14.194  fun mk_completeness names glrs =
  14.195      let
  14.196 -	val Names {domT, x, Pbool, ...} = names
  14.197 +        val Names {domT, x, Pbool, ...} = names
  14.198  
  14.199 -	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
  14.200 -						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
  14.201 -						|> fold_rev (curry Logic.mk_implies) gs
  14.202 -						|> fold_rev mk_forall qs
  14.203 +        fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
  14.204 +                                                |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
  14.205 +                                                |> fold_rev (curry Logic.mk_implies) gs
  14.206 +                                                |> fold_rev mk_forall qs
  14.207      in
  14.208 -	Trueprop Pbool
  14.209 -		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
  14.210 +        Trueprop Pbool
  14.211 +                 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
  14.212                   |> mk_forall_rename (x, "x")
  14.213                   |> mk_forall_rename (Pbool, "P")
  14.214      end
  14.215  
  14.216  
  14.217 -fun inductive_def_wrap defs (thy, const) = 
  14.218 -    let 
  14.219 +fun inductive_def_wrap defs (thy, const) =
  14.220 +    let
  14.221        val qdefs = map dest_all_all defs
  14.222  
  14.223 -      val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) = 
  14.224 -	  InductivePackage.add_inductive_i true (*verbose*)
  14.225 -					     false (*add_consts*)
  14.226 -					     "" (* no altname *)
  14.227 -					     false (* no coind *)
  14.228 -					     false (* elims, please *)
  14.229 -					     false (* induction thm please *)
  14.230 -					     [const] (* the constant *)
  14.231 -					     (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
  14.232 -					     [] (* no special monos *)
  14.233 -					     thy
  14.234 +      val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
  14.235 +          InductivePackage.add_inductive_i true (*verbose*)
  14.236 +                                             false (*add_consts*)
  14.237 +                                             "" (* no altname *)
  14.238 +                                             false (* no coind *)
  14.239 +                                             false (* elims, please *)
  14.240 +                                             false (* induction thm please *)
  14.241 +                                             [const] (* the constant *)
  14.242 +                                             (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
  14.243 +                                             [] (* no special monos *)
  14.244 +                                             thy
  14.245  
  14.246  (* It would be nice if this worked... But this is actually HO-Unification... *)
  14.247  (*      fun inst (qs, intr) intr_gen =
  14.248 @@ -191,7 +187,7 @@
  14.249                      |> fold_rev (forall_intr o cterm_of thy) qs*)
  14.250  
  14.251        fun inst (qs, intr) intr_gen =
  14.252 -          intr_gen 
  14.253 +          intr_gen
  14.254              |> Thm.freezeT
  14.255              |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs
  14.256  
  14.257 @@ -208,10 +204,10 @@
  14.258  
  14.259  
  14.260  (*
  14.261 - * "!!qs xs. CS ==> G => (r, lhs) : R" 
  14.262 + * "!!qs xs. CS ==> G => (r, lhs) : R"
  14.263   *)
  14.264  fun mk_RIntro R (qs, gs, lhs, rhs) (rcfix, rcassm, rcarg) =
  14.265 -    mk_relmem (rcarg, lhs) R 
  14.266 +    mk_relmem (rcarg, lhs) R
  14.267                |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  14.268                |> fold_rev (curry Logic.mk_implies) gs
  14.269                |> fold_rev (mk_forall o Free) rcfix
  14.270 @@ -236,32 +232,32 @@
  14.271  
  14.272  fun mk_clause_info thy names no (qs,gs,lhs,rhs) tree RCs GIntro_thm RIntro_thms =
  14.273      let
  14.274 -	val Names {G, h, f, fvar, x, ...} = names 
  14.275 -				 
  14.276 -	val cqs = map (cterm_of thy) qs
  14.277 -	val ags = map (assume o cterm_of thy) gs
  14.278 +        val Names {G, h, f, fvar, x, ...} = names
  14.279 +
  14.280 +        val cqs = map (cterm_of thy) qs
  14.281 +        val ags = map (assume o cterm_of thy) gs
  14.282  
  14.283          val used = [] (* XXX *)
  14.284                    (* FIXME: What is the relationship between this and mk_primed_vars? *)
  14.285 -	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
  14.286 -	val cqs' = map (cterm_of thy) qs'
  14.287 +        val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
  14.288 +        val cqs' = map (cterm_of thy) qs'
  14.289  
  14.290 -	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
  14.291 -	val ags' = map (assume o cterm_of thy o rename_vars) gs
  14.292 -	val lhs' = rename_vars lhs
  14.293 -	val rhs' = rename_vars rhs
  14.294 +        val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
  14.295 +        val ags' = map (assume o cterm_of thy o rename_vars) gs
  14.296 +        val lhs' = rename_vars lhs
  14.297 +        val rhs' = rename_vars rhs
  14.298  
  14.299          val lGI = GIntro_thm
  14.300                      |> forall_elim (cterm_of thy f)
  14.301                      |> fold forall_elim cqs
  14.302                      |> fold implies_elim_swp ags
  14.303 -		
  14.304 +
  14.305          (* FIXME: Can be removed when inductive-package behaves nicely. *)
  14.306 -        val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) []) 
  14.307 +        val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [])
  14.308                            (term_frees (snd (dest_all_all (prop_of GIntro_thm))))
  14.309 -               	  
  14.310 -	fun mk_call_info (rcfix, rcassm, rcarg) RI =
  14.311 -	    let
  14.312 +
  14.313 +        fun mk_call_info (rcfix, rcassm, rcarg) RI =
  14.314 +            let
  14.315                  val crcfix = map (cterm_of thy o Free) rcfix
  14.316  
  14.317                  val llRI = RI
  14.318 @@ -270,32 +266,32 @@
  14.319                               |> fold implies_elim_swp ags
  14.320                               |> fold implies_elim_swp rcassm
  14.321  
  14.322 -                val h_assum = 
  14.323 +                val h_assum =
  14.324                      mk_relmem (rcarg, h $ rcarg) G
  14.325                                |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  14.326                                |> fold_rev (mk_forall o Free) rcfix
  14.327                                |> Pattern.rewrite_term thy [(f, h)] []
  14.328  
  14.329 -		val Gh = assume (cterm_of thy h_assum)
  14.330 -		val Gh' = assume (cterm_of thy (rename_vars h_assum))
  14.331 -	    in
  14.332 -		RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
  14.333 -	    end
  14.334 +                val Gh = assume (cterm_of thy h_assum)
  14.335 +                val Gh' = assume (cterm_of thy (rename_vars h_assum))
  14.336 +            in
  14.337 +                RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
  14.338 +            end
  14.339  
  14.340 -	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
  14.341 +        val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
  14.342  
  14.343          val RC_infos = map2 mk_call_info RCs RIntro_thms
  14.344      in
  14.345 -	ClauseInfo
  14.346 -	    {
  14.347 -	     no=no,
  14.348 -	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
  14.349 -	     cqs=cqs, ags=ags,		 
  14.350 -	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', 
  14.351 -	     lGI=lGI, RCs=RC_infos,
  14.352 -	     tree=tree, case_hyp = case_hyp,
  14.353 +        ClauseInfo
  14.354 +            {
  14.355 +             no=no,
  14.356 +             qs=qs, gs=gs, lhs=lhs, rhs=rhs,
  14.357 +             cqs=cqs, ags=ags,
  14.358 +             cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs',
  14.359 +             lGI=lGI, RCs=RC_infos,
  14.360 +             tree=tree, case_hyp = case_hyp,
  14.361               ordcqs'=ordcqs'
  14.362 -	    }
  14.363 +            }
  14.364      end
  14.365  
  14.366  
  14.367 @@ -311,9 +307,9 @@
  14.368  fun store_compat_thms 0 thms = []
  14.369    | store_compat_thms n thms =
  14.370      let
  14.371 -	val (thms1, thms2) = chop n thms
  14.372 +        val (thms1, thms2) = chop n thms
  14.373      in
  14.374 -	(thms1 :: store_compat_thms (n - 1) thms2)
  14.375 +        (thms1 :: store_compat_thms (n - 1) thms2)
  14.376      end
  14.377  
  14.378  
  14.379 @@ -326,32 +322,32 @@
  14.380  (* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
  14.381  (* if j < i, then turn around *)
  14.382  fun get_compat_thm thy cts clausei clausej =
  14.383 -    let 
  14.384 -	val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
  14.385 -	val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
  14.386 +    let
  14.387 +        val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
  14.388 +        val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
  14.389  
  14.390 -	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
  14.391 +        val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
  14.392      in if j < i then
  14.393 -	   let 
  14.394 -	       val compat = lookup_compat_thm j i cts
  14.395 -	   in
  14.396 -	       compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
  14.397 +           let
  14.398 +               val compat = lookup_compat_thm j i cts
  14.399 +           in
  14.400 +               compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
  14.401                  |> fold forall_elim (qsj' @ qsi) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
  14.402 -		|> fold implies_elim_swp gsj'
  14.403 -		|> fold implies_elim_swp gsi
  14.404 -		|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
  14.405 -	   end
  14.406 +                |> fold implies_elim_swp gsj'
  14.407 +                |> fold implies_elim_swp gsi
  14.408 +                |> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
  14.409 +           end
  14.410         else
  14.411 -	   let
  14.412 -	       val compat = lookup_compat_thm i j cts
  14.413 -	   in
  14.414 -	       compat        (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
  14.415 +           let
  14.416 +               val compat = lookup_compat_thm i j cts
  14.417 +           in
  14.418 +               compat        (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
  14.419                   |> fold forall_elim (qsi @ qsj') (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
  14.420 -		 |> fold implies_elim_swp gsi
  14.421 -		 |> fold implies_elim_swp gsj'
  14.422 -		 |> implies_elim_swp (assume lhsi_eq_lhsj')
  14.423 -		 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
  14.424 -	   end
  14.425 +                 |> fold implies_elim_swp gsi
  14.426 +                 |> fold implies_elim_swp gsj'
  14.427 +                 |> implies_elim_swp (assume lhsi_eq_lhsj')
  14.428 +                 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
  14.429 +           end
  14.430      end
  14.431  
  14.432  
  14.433 @@ -359,29 +355,29 @@
  14.434  (* Generates the replacement lemma with primed variables. A problem here is that one should not do
  14.435  the complete requantification at the end to replace the variables. One should find a way to be more efficient
  14.436  here. *)
  14.437 -fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
  14.438 -    let 
  14.439 -	val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
  14.440 -	val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
  14.441 +fun mk_replacement_lemma thy (names:naming_context) ih_elim clause =
  14.442 +    let
  14.443 +        val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
  14.444 +        val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
  14.445  
  14.446 -	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
  14.447 +        val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
  14.448  
  14.449 -	val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
  14.450 -	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
  14.451 -	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
  14.452 +        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
  14.453 +        val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
  14.454 +        val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
  14.455  
  14.456 -	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
  14.457 +        val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
  14.458  
  14.459 -	val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
  14.460 +        val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
  14.461  
  14.462 -	val replace_lemma = (eql RS meta_eq_to_obj_eq)
  14.463 -				|> implies_intr (cprop_of case_hyp)
  14.464 -				|> fold_rev (implies_intr o cprop_of) h_assums
  14.465 -				|> fold_rev (implies_intr o cprop_of) ags
  14.466 -				|> fold_rev forall_intr cqs
  14.467 -				|> fold forall_elim cqs'
  14.468 -				|> fold implies_elim_swp ags'
  14.469 -				|> fold implies_elim_swp h_assums'
  14.470 +        val replace_lemma = (eql RS meta_eq_to_obj_eq)
  14.471 +                                |> implies_intr (cprop_of case_hyp)
  14.472 +                                |> fold_rev (implies_intr o cprop_of) h_assums
  14.473 +                                |> fold_rev (implies_intr o cprop_of) ags
  14.474 +                                |> fold_rev forall_intr cqs
  14.475 +                                |> fold forall_elim cqs'
  14.476 +                                |> fold implies_elim_swp ags'
  14.477 +                                |> fold implies_elim_swp h_assums'
  14.478      in
  14.479        replace_lemma
  14.480      end
  14.481 @@ -391,84 +387,84 @@
  14.482  
  14.483  fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
  14.484      let
  14.485 -	val Names {f, h, y, ...} = names
  14.486 -	val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
  14.487 -	val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
  14.488 +        val Names {f, h, y, ...} = names
  14.489 +        val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
  14.490 +        val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
  14.491  
  14.492 -	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
  14.493 -	val compat = get_compat_thm thy compat_store clausei clausej
  14.494 -	val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
  14.495 +        val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
  14.496 +        val compat = get_compat_thm thy compat_store clausei clausej
  14.497 +        val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
  14.498  
  14.499 -	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
  14.500 -	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
  14.501 +        val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
  14.502 +        val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
  14.503  
  14.504 -	val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
  14.505 +        val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
  14.506      in
  14.507 -	(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
  14.508 +        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
  14.509          |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
  14.510 -	|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
  14.511 -	|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
  14.512 -	|> implies_intr (cprop_of y_eq_rhsj'h)
  14.513 -	|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
  14.514 -	|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  14.515 -	|> implies_elim_swp eq_pairs
  14.516 -	|> fold_rev (implies_intr o cprop_of) Ghsj' 
  14.517 -	|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  14.518 -	|> implies_intr (cprop_of eq_pairs)
  14.519 -	|> fold_rev forall_intr ordcqs'j
  14.520 +        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
  14.521 +        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
  14.522 +        |> implies_intr (cprop_of y_eq_rhsj'h)
  14.523 +        |> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
  14.524 +        |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  14.525 +        |> implies_elim_swp eq_pairs
  14.526 +        |> fold_rev (implies_intr o cprop_of) Ghsj'
  14.527 +        |> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
  14.528 +        |> implies_intr (cprop_of eq_pairs)
  14.529 +        |> fold_rev forall_intr ordcqs'j
  14.530      end
  14.531  
  14.532  
  14.533  
  14.534  fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
  14.535      let
  14.536 -	val Names {x, y, G, fvar, f, ranT, ...} = names
  14.537 -	val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
  14.538 +        val Names {x, y, G, fvar, f, ranT, ...} = names
  14.539 +        val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
  14.540  
  14.541 -	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
  14.542 +        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
  14.543  
  14.544 -	fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
  14.545 +        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
  14.546                                                              |> fold_rev (implies_intr o cprop_of) CCas
  14.547 -						            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  14.548 +                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  14.549  
  14.550 -	val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
  14.551 -			    |> fold (curry op COMP o prep_RC) RCs 
  14.552 +        val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
  14.553 +                            |> fold (curry op COMP o prep_RC) RCs
  14.554  
  14.555 -	val a = cterm_of thy (mk_prod (lhs, y))
  14.556 -	val P = cterm_of thy (mk_eq (y, rhs))
  14.557 -	val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
  14.558 +        val a = cterm_of thy (mk_prod (lhs, y))
  14.559 +        val P = cterm_of thy (mk_eq (y, rhs))
  14.560 +        val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
  14.561  
  14.562 -	val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
  14.563 +        val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
  14.564  
  14.565 -	val uniqueness = G_cases 
  14.566 +        val uniqueness = G_cases
  14.567                             |> forall_elim a
  14.568                             |> forall_elim P
  14.569 -			   |> implies_elim_swp a_in_G
  14.570 -			   |> fold implies_elim_swp unique_clauses
  14.571 -			   |> implies_intr (cprop_of a_in_G)
  14.572 -			   |> forall_intr (cterm_of thy y) 
  14.573 +                           |> implies_elim_swp a_in_G
  14.574 +                           |> fold implies_elim_swp unique_clauses
  14.575 +                           |> implies_intr (cprop_of a_in_G)
  14.576 +                           |> forall_intr (cterm_of thy y)
  14.577  
  14.578 -	val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
  14.579 +        val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
  14.580  
  14.581 -	val exactly_one =
  14.582 -	    ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
  14.583 -		 |> curry (op COMP) existence
  14.584 -		 |> curry (op COMP) uniqueness
  14.585 -		 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
  14.586 -		 |> implies_intr (cprop_of case_hyp) 
  14.587 -		 |> fold_rev (implies_intr o cprop_of) ags
  14.588 -		 |> fold_rev forall_intr cqs
  14.589 +        val exactly_one =
  14.590 +            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
  14.591 +                 |> curry (op COMP) existence
  14.592 +                 |> curry (op COMP) uniqueness
  14.593 +                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
  14.594 +                 |> implies_intr (cprop_of case_hyp)
  14.595 +                 |> fold_rev (implies_intr o cprop_of) ags
  14.596 +                 |> fold_rev forall_intr cqs
  14.597  
  14.598 -	val function_value =
  14.599 -	    existence 
  14.600 -		|> fold_rev (implies_intr o cprop_of) ags
  14.601 -		|> implies_intr ihyp
  14.602 -		|> implies_intr (cprop_of case_hyp)
  14.603 -		|> forall_intr (cterm_of thy x)
  14.604 -		|> forall_elim (cterm_of thy lhs)
  14.605 -		|> curry (op RS) refl
  14.606 +        val function_value =
  14.607 +            existence
  14.608 +                |> fold_rev (implies_intr o cprop_of) ags
  14.609 +                |> implies_intr ihyp
  14.610 +                |> implies_intr (cprop_of case_hyp)
  14.611 +                |> forall_intr (cterm_of thy x)
  14.612 +                |> forall_elim (cterm_of thy lhs)
  14.613 +                |> curry (op RS) refl
  14.614      in
  14.615 -	(exactly_one, function_value)
  14.616 +        (exactly_one, function_value)
  14.617      end
  14.618  
  14.619  
  14.620 @@ -476,45 +472,45 @@
  14.621  
  14.622  fun prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim =
  14.623      let
  14.624 -	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
  14.625 +        val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
  14.626 +
  14.627 +        val f_def_fr = Thm.freezeT f_def
  14.628  
  14.629 -	val f_def_fr = Thm.freezeT f_def
  14.630 +        val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)]
  14.631 +                                                [SOME (cterm_of thy f), SOME (cterm_of thy G)])
  14.632 +                                      #> curry op COMP (forall_intr_vars f_def_fr)
  14.633  
  14.634 -	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
  14.635 -						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
  14.636 -				      #> curry op COMP (forall_intr_vars f_def_fr)
  14.637 -			  
  14.638 -	val inst_ex1_ex = instantiate_and_def ex1_implies_ex
  14.639 -	val inst_ex1_un = instantiate_and_def ex1_implies_un
  14.640 -	val inst_ex1_iff = instantiate_and_def ex1_implies_iff
  14.641 +        val inst_ex1_ex = instantiate_and_def ex1_implies_ex
  14.642 +        val inst_ex1_un = instantiate_and_def ex1_implies_un
  14.643 +        val inst_ex1_iff = instantiate_and_def ex1_implies_iff
  14.644 +
  14.645 +        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
  14.646 +        val ihyp = all domT $ Abs ("z", domT,
  14.647 +                                   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
  14.648 +                                           $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
  14.649 +                                                             Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
  14.650 +                       |> cterm_of thy
  14.651  
  14.652 -	(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
  14.653 -	val ihyp = all domT $ Abs ("z", domT, 
  14.654 -				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
  14.655 -					   $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
  14.656 -							     Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
  14.657 -		       |> cterm_of thy
  14.658 -		   
  14.659 -	val ihyp_thm = assume ihyp |> forall_elim_vars 0
  14.660 -	val ih_intro = ihyp_thm RS inst_ex1_ex
  14.661 -	val ih_elim = ihyp_thm RS inst_ex1_un
  14.662 +        val ihyp_thm = assume ihyp |> forall_elim_vars 0
  14.663 +        val ih_intro = ihyp_thm RS inst_ex1_ex
  14.664 +        val ih_elim = ihyp_thm RS inst_ex1_un
  14.665  
  14.666 -	val _ = Output.debug "Proving Replacement lemmas..."
  14.667 -	val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
  14.668 +        val _ = Output.debug "Proving Replacement lemmas..."
  14.669 +        val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
  14.670 +
  14.671 +        val _ = Output.debug "Proving cases for unique existence..."
  14.672 +        val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
  14.673  
  14.674 -	val _ = Output.debug "Proving cases for unique existence..."
  14.675 -	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
  14.676 -
  14.677 -	val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
  14.678 -	val graph_is_function = complete 
  14.679 +        val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
  14.680 +        val graph_is_function = complete
  14.681                                    |> forall_elim_vars 0
  14.682 -				  |> fold (curry op COMP) ex1s
  14.683 -				  |> implies_intr (ihyp)
  14.684 -				  |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
  14.685 -				  |> forall_intr (cterm_of thy x)
  14.686 -				  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
  14.687 +                                  |> fold (curry op COMP) ex1s
  14.688 +                                  |> implies_intr (ihyp)
  14.689 +                                  |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
  14.690 +                                  |> forall_intr (cterm_of thy x)
  14.691 +                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
  14.692                                    |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
  14.693 -				  |> Drule.close_derivation
  14.694 +                                  |> Drule.close_derivation
  14.695  
  14.696          val goal = complete COMP (graph_is_function COMP conjunctionI)
  14.697                              |> Drule.close_derivation
  14.698 @@ -539,9 +535,9 @@
  14.699  fun prepare_fundef thy congs defname f qglrs used =
  14.700      let
  14.701        val (names, thy) = setup_context f qglrs defname thy
  14.702 -      val Names {G, R, ctx, glrs', fvar, ...} = names 
  14.703 +      val Names {G, R, ctx, glrs', fvar, ...} = names
  14.704  
  14.705 -                         
  14.706 +
  14.707        val n = length qglrs
  14.708        val trees = map (build_tree thy f congs ctx) qglrs
  14.709        val RCss = map find_calls trees
  14.710 @@ -558,16 +554,16 @@
  14.711  
  14.712        val R_intross = map2 (fn qglr => map (mk_RIntro R qglr)) qglrs RCss
  14.713        val G_intros = map2 (mk_GIntro thy f fvar G) qglrs RCss
  14.714 -                    
  14.715 +
  14.716        val (GIntro_thms, (thy, _, G_elim)) = inductive_def_wrap G_intros (thy, G)
  14.717        val (RIntro_thmss, (thy, _, R_elim)) = fold_burrow inductive_def_wrap R_intross (thy, R)
  14.718 - 
  14.719 +
  14.720        val clauses = map6 (mk_clause_info thy names) (1 upto n) qglrs trees RCss GIntro_thms RIntro_thmss
  14.721 -                  
  14.722 +
  14.723        val (goal, goalI, ex1_iff, values) = prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim
  14.724      in
  14.725 -	(Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
  14.726 -	 thy) 
  14.727 +        (Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
  14.728 +         thy)
  14.729      end
  14.730  
  14.731  
    15.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Jul 11 12:16:52 2006 +0200
    15.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jul 11 12:16:54 2006 +0200
    15.3 @@ -343,7 +343,7 @@
    15.4  
    15.5  fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
    15.6        NONE => ((names, (s, [s])::vs), s)
    15.7 -    | SOME xs => let val s' = variant names s in
    15.8 +    | SOME xs => let val s' = Name.variant names s in
    15.9          ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
   15.10  
   15.11  fun distinct_v (nvs, Var ((s, 0), T)) =
   15.12 @@ -407,7 +407,7 @@
   15.13  
   15.14      fun check_constrt ((names, eqs), t) =
   15.15        if is_constrt thy t then ((names, eqs), t) else
   15.16 -        let val s = variant names "x";
   15.17 +        let val s = Name.variant names "x";
   15.18          in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
   15.19  
   15.20      fun compile_eq (gr, (s, t)) =
    16.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jul 11 12:16:52 2006 +0200
    16.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jul 11 12:16:54 2006 +0200
    16.3 @@ -324,7 +324,7 @@
    16.4  fun mk_elims cs cTs params intr_ts intr_names =
    16.5    let
    16.6      val used = foldr add_term_names [] intr_ts;
    16.7 -    val [aname, pname] = variantlist (["a", "P"], used);
    16.8 +    val [aname, pname] = Name.variant_list used ["a", "P"];
    16.9      val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   16.10  
   16.11      fun dest_intr r =
   16.12 @@ -359,8 +359,8 @@
   16.13  
   16.14      (* predicates for induction rule *)
   16.15  
   16.16 -    val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   16.17 -      map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   16.18 +    val preds = map Free (Name.variant_list used (if length cs < 2 then ["P"] else
   16.19 +      map (fn i => "P" ^ string_of_int i) (1 upto length cs)) ~~
   16.20          map (fn T => T --> HOLogic.boolT) cTs);
   16.21  
   16.22      (* transform an introduction rule into a premise for induction rule *)
   16.23 @@ -697,7 +697,7 @@
   16.24      val fp_name = if coind then gfp_name else lfp_name;
   16.25  
   16.26      val used = foldr add_term_names [] intr_ts;
   16.27 -    val [sname, xname] = variantlist (["S", "x"], used);
   16.28 +    val [sname, xname] = Name.variant_list used ["S", "x"];
   16.29  
   16.30      (* transform an introduction rule into a conjunction  *)
   16.31      (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
    17.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 11 12:16:52 2006 +0200
    17.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 11 12:16:54 2006 +0200
    17.3 @@ -35,7 +35,7 @@
    17.4  fun strip_all t =
    17.5    let
    17.6      fun strip used (Const ("all", _) $ Abs (s, T, t)) =
    17.7 -          let val s' = variant used s
    17.8 +          let val s' = Name.variant used s
    17.9            in strip (s'::used) (subst_bound (Free (s', T), t)) end
   17.10        | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
   17.11        | strip _ t = t;
   17.12 @@ -152,7 +152,7 @@
   17.13      fun fun_of ts rts args used (prem :: prems) =
   17.14            let
   17.15              val T = Extraction.etype_of thy vs [] prem;
   17.16 -            val [x, r] = variantlist (["x", "r"], used)
   17.17 +            val [x, r] = Name.variant_list used ["x", "r"]
   17.18            in if T = Extraction.nullT
   17.19              then fun_of ts rts args used prems
   17.20              else if is_rec prem then
   17.21 @@ -248,7 +248,7 @@
   17.22      handle DatatypeAux.Datatype_Empty name' =>
   17.23        let
   17.24          val name = Sign.base_name name';
   17.25 -        val dname = variant used "Dummy"
   17.26 +        val dname = Name.variant used "Dummy"
   17.27        in
   17.28          thy
   17.29          |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
    18.1 --- a/src/HOL/Tools/record_package.ML	Tue Jul 11 12:16:52 2006 +0200
    18.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jul 11 12:16:54 2006 +0200
    18.3 @@ -1315,7 +1315,7 @@
    18.4      val fieldTs = (map snd fields);
    18.5      val alphas_zeta = alphas@[zeta];
    18.6      val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
    18.7 -    val vT = TFree (variant alphas_zeta "'v", HOLogic.typeS);
    18.8 +    val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
    18.9      val extT_name = suffix ext_typeN name
   18.10      val extT = Type (extT_name, alphas_zetaTs);
   18.11      val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]);
   18.12 @@ -1385,8 +1385,8 @@
   18.13      val ext = mk_ext vars_more;
   18.14      val s     = Free (rN, extT);
   18.15      val w     = Free (wN, extT);
   18.16 -    val P = Free (variant variants "P", extT-->HOLogic.boolT);
   18.17 -    val C = Free (variant variants "C", HOLogic.boolT);
   18.18 +    val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
   18.19 +    val C = Free (Name.variant variants "C", HOLogic.boolT);
   18.20  
   18.21      val inject_prop =
   18.22        let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
   18.23 @@ -1411,7 +1411,7 @@
   18.24  
   18.25      (*updates*)
   18.26      fun mk_upd_prop (i,(c,T)) =
   18.27 -      let val x' = Free (variant variants (base c ^ "'"),T)
   18.28 +      let val x' = Free (Name.variant variants (base c ^ "'"),T)
   18.29            val args' = nth_update (i, x') vars_more
   18.30        in mk_upd updN c x' ext === mk_ext args'  end;
   18.31      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
   18.32 @@ -1422,7 +1422,7 @@
   18.33        in s === mk_ext args end;
   18.34  
   18.35      val split_meta_prop =
   18.36 -      let val P = Free (variant variants "P", extT-->Term.propT) in
   18.37 +      let val P = Free (Name.variant variants "P", extT-->Term.propT) in
   18.38          Logic.mk_equals
   18.39           (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
   18.40        end;
   18.41 @@ -1479,7 +1479,7 @@
   18.42      fun upd_convs_prf_opt () =
   18.43        let
   18.44          fun mkrefl (c,T) = Thm.reflexive
   18.45 -                            (cterm_of defs_thy (Free (variant variants (base c ^ "'"),T)));
   18.46 +                            (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T)));
   18.47          val refls = map mkrefl fields_more;
   18.48          val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
   18.49          val dest_convs' = map mk_meta_eq dest_convs;
   18.50 @@ -1595,7 +1595,7 @@
   18.51      val parent_names = map fst parent_fields;
   18.52      val parent_types = map snd parent_fields;
   18.53      val parent_fields_len = length parent_fields;
   18.54 -    val parent_variants = variantlist (map base parent_names, [moreN, rN, rN ^ "'", wN]);
   18.55 +    val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
   18.56      val parent_vars = ListPair.map Free (parent_variants, parent_types);
   18.57      val parent_len = length parents;
   18.58      val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
   18.59 @@ -1607,7 +1607,7 @@
   18.60      val alphas_fields = foldr add_typ_tfree_names [] types;
   18.61      val alphas_ext = alphas inter alphas_fields;
   18.62      val len = length fields;
   18.63 -    val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::wN::parent_variants);
   18.64 +    val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields);
   18.65      val vars = ListPair.map Free (variants, types);
   18.66      val named_vars = names ~~ vars;
   18.67      val idxs = 0 upto (len - 1);
   18.68 @@ -1622,7 +1622,7 @@
   18.69      val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
   18.70  
   18.71  
   18.72 -    val zeta = variant alphas "'z";
   18.73 +    val zeta = Name.variant alphas "'z";
   18.74      val moreT = TFree (zeta, HOLogic.typeS);
   18.75      val more = Free (moreN, moreT);
   18.76      val full_moreN = full moreN;
   18.77 @@ -1779,9 +1779,9 @@
   18.78  
   18.79      (* prepare propositions *)
   18.80      val _ = timing_msg "record preparing propositions";
   18.81 -    val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
   18.82 -    val C = Free (variant all_variants "C", HOLogic.boolT);
   18.83 -    val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT);
   18.84 +    val P = Free (Name.variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
   18.85 +    val C = Free (Name.variant all_variants "C", HOLogic.boolT);
   18.86 +    val P_unit = Free (Name.variant all_variants "P", recT0-->HOLogic.boolT);
   18.87  
   18.88      (*selectors*)
   18.89      val sel_conv_props =
   18.90 @@ -1789,7 +1789,7 @@
   18.91  
   18.92      (*updates*)
   18.93      fun mk_upd_prop (i,(c,T)) =
   18.94 -      let val x' = Free (variant all_variants (base c ^ "'"),T)
   18.95 +      let val x' = Free (Name.variant all_variants (base c ^ "'"),T)
   18.96            val args' = nth_update (parent_fields_len + i, x') all_vars_more
   18.97        in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
   18.98      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
   18.99 @@ -1819,7 +1819,7 @@
  18.100  
  18.101      (*split*)
  18.102      val split_meta_prop =
  18.103 -      let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in
  18.104 +      let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
  18.105          Logic.mk_equals
  18.106           (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
  18.107        end;
    19.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Jul 11 12:16:52 2006 +0200
    19.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Jul 11 12:16:54 2006 +0200
    19.3 @@ -145,7 +145,7 @@
    19.4  	    end
    19.5  	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) =
    19.6  	    (*Universal quant: insert a free variable into body and continue*)
    19.7 -	    let val fname = variant (add_term_names (p,[])) a
    19.8 +	    let val fname = Name.variant (add_term_names (p,[])) a
    19.9  	    in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end
   19.10  	| dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
   19.11  	| dec_sko (Const ("op |", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
   19.12 @@ -157,7 +157,7 @@
   19.13  fun assume_skofuns th =
   19.14    let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
   19.15  	    (*Existential: declare a Skolem function, then insert into body and continue*)
   19.16 -	    let val name = variant (add_term_names (p,[])) (gensym "sko_")
   19.17 +	    let val name = Name.variant (add_term_names (p,[])) (gensym "sko_")
   19.18                  val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
   19.19  		val args = term_frees xtp \\ skos  (*the formal parameters*)
   19.20  		val Ts = map type_of args
   19.21 @@ -172,7 +172,7 @@
   19.22  	    end
   19.23  	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
   19.24  	    (*Universal quant: insert a free variable into body and continue*)
   19.25 -	    let val fname = variant (add_term_names (p,[])) a
   19.26 +	    let val fname = Name.variant (add_term_names (p,[])) a
   19.27  	    in dec_sko (subst_bound (Free(fname,T), p)) defs end
   19.28  	| dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
   19.29  	| dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
    20.1 --- a/src/HOL/Tools/split_rule.ML	Tue Jul 11 12:16:52 2006 +0200
    20.2 +++ b/src/HOL/Tools/split_rule.ML	Tue Jul 11 12:16:54 2006 +0200
    20.3 @@ -81,7 +81,7 @@
    20.4          fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
    20.5                let
    20.6                  val Ts = HOLogic.prodT_factors T;
    20.7 -                val ys = Term.variantlist (replicate (length Ts) a, xs);
    20.8 +                val ys = Name.variant_list xs (replicate (length Ts) a);
    20.9                in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
   20.10                  (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
   20.11                end
    21.1 --- a/src/HOLCF/domain/theorems.ML	Tue Jul 11 12:16:52 2006 +0200
    21.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Jul 11 12:16:54 2006 +0200
    21.3 @@ -476,7 +476,7 @@
    21.4            val arg1 = (con1, args1);
    21.5            val arg2 =
    21.6              (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
    21.7 -              (args2, variantlist (map vname args2,map vname args1)));
    21.8 +              (args2, Name.variant_list (map vname args1) (map vname args2)));
    21.9          in [dist arg1 arg2, dist arg2 arg1] end;
   21.10      fun distincts []      = []
   21.11        | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
    22.1 --- a/src/HOLCF/fixrec_package.ML	Tue Jul 11 12:16:52 2006 +0200
    22.2 +++ b/src/HOLCF/fixrec_package.ML	Tue Jul 11 12:16:54 2006 +0200
    22.3 @@ -142,7 +142,7 @@
    22.4        in pre_build f rhs' (v::vs) taken' end
    22.5    | Const(c,T) =>
    22.6        let
    22.7 -        val n = variant taken "v";
    22.8 +        val n = Name.variant taken "v";
    22.9          fun result_type (Type("Cfun.->",[_,T])) (x::xs) = result_type T xs
   22.10            | result_type T _ = T;
   22.11          val v = Free(n, result_type T vs);
    23.1 --- a/src/Provers/IsaPlanner/isand.ML	Tue Jul 11 12:16:52 2006 +0200
    23.2 +++ b/src/Provers/IsaPlanner/isand.ML	Tue Jul 11 12:16:54 2006 +0200
    23.3 @@ -204,7 +204,7 @@
    23.4        val tvars = List.foldr Term.add_term_tvars [] ts;
    23.5        val (names',renamings) = 
    23.6            List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
    23.7 -                         let val n2 = Term.variant Ns n in 
    23.8 +                         let val n2 = Name.variant Ns n in 
    23.9                             (n2::Ns, (tv, (n2,s))::Rs)
   23.10                           end) (tfree_names @ names,[]) tvars;
   23.11      in renamings end;
   23.12 @@ -237,7 +237,7 @@
   23.13        val Ns = List.foldr Term.add_term_names names ts;
   23.14        val (_,renamings) = 
   23.15            Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   23.16 -                    let val n2 = Term.variant Ns n in
   23.17 +                    let val n2 = Name.variant Ns n in
   23.18                        (n2 :: Ns, (v, (n2,ty)) :: Rs)
   23.19                      end) ((Ns,[]), vars);
   23.20      in renamings end;
   23.21 @@ -436,7 +436,7 @@
   23.22        val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   23.23        val names = Term.add_term_names (t,varnames);
   23.24        val fvs = map Free 
   23.25 -                    ((Term.variantlist (map fst alls, names)) 
   23.26 +                    (Name.variant_list names (map fst alls)
   23.27                         ~~ (map snd alls));
   23.28      in ((subst_bounds (fvs,t)), fvs) end;
   23.29  
   23.30 @@ -448,7 +448,7 @@
   23.31        val body = Term.strip_all_body gt;
   23.32        val alls = rev (Term.strip_all_vars gt);
   23.33        val fvs = map Free 
   23.34 -                    ((Term.variantlist (map fst alls, names)) 
   23.35 +                    (Name.variant_list names (map fst alls)
   23.36                         ~~ (map snd alls));
   23.37      in ((subst_bounds (fvs,body)), fvs) end;
   23.38  
    24.1 --- a/src/Provers/IsaPlanner/rw_inst.ML	Tue Jul 11 12:16:52 2006 +0200
    24.2 +++ b/src/Provers/IsaPlanner/rw_inst.ML	Tue Jul 11 12:16:54 2006 +0200
    24.3 @@ -109,7 +109,7 @@
    24.4        val names = usednames_of_thm rule;
    24.5        val (fromnames,tonames,names2,Ts') = 
    24.6            Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
    24.7 -                    let val n2 = Term.variant names n in
    24.8 +                    let val n2 = Name.variant names n in
    24.9                        (ctermify (Free(faken,ty)) :: rnf,
   24.10                         ctermify (Free(n2,ty)) :: rnt, 
   24.11                         n2 :: names,
   24.12 @@ -156,7 +156,7 @@
   24.13        val vars_to_fix = Library.union (termvars, cond_vs);
   24.14        val (renamings, names2) = 
   24.15            foldr (fn (((n,i),ty), (vs, names')) => 
   24.16 -                    let val n' = Term.variant names' n in
   24.17 +                    let val n' = Name.variant names' n in
   24.18                        ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   24.19                      end)
   24.20                  ([], names) vars_to_fix;
   24.21 @@ -164,7 +164,7 @@
   24.22  
   24.23  (* make a new fresh typefree instantiation for the given tvar *)
   24.24  fun new_tfree (tv as (ix,sort), (pairs,used)) =
   24.25 -      let val v = variant used (string_of_indexname ix)
   24.26 +      let val v = Name.variant used (string_of_indexname ix)
   24.27        in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
   24.28  
   24.29  
    25.1 --- a/src/Provers/eqsubst.ML	Tue Jul 11 12:16:52 2006 +0200
    25.2 +++ b/src/Provers/eqsubst.ML	Tue Jul 11 12:16:54 2006 +0200
    25.3 @@ -180,7 +180,7 @@
    25.4  fun fakefree_badbounds Ts t = 
    25.5      let val (FakeTs,Ts,newnames) = 
    25.6              List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
    25.7 -                           let val newname = Term.variant usednames n
    25.8 +                           let val newname = Name.variant usednames n
    25.9                             in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   25.10                                 (newname,ty)::Ts, 
   25.11                                 newname::usednames) end)
    26.1 --- a/src/Pure/Proof/proofchecker.ML	Tue Jul 11 12:16:52 2006 +0200
    26.2 +++ b/src/Pure/Proof/proofchecker.ML	Tue Jul 11 12:16:54 2006 +0200
    26.3 @@ -62,7 +62,7 @@
    26.4  
    26.5        | thm_of vs Hs (Abst (s, SOME T, prf)) =
    26.6            let
    26.7 -            val x = variant (names @ map fst vs) s;
    26.8 +            val x = Name.variant (names @ map fst vs) s;
    26.9              val thm = thm_of ((x, T) :: vs) Hs prf
   26.10            in
   26.11              Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
    27.1 --- a/src/Pure/Tools/codegen_thingol.ML	Tue Jul 11 12:16:52 2006 +0200
    27.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Tue Jul 11 12:16:54 2006 +0200
    27.3 @@ -370,7 +370,7 @@
    27.4  
    27.5  fun invent seed used =
    27.6    let
    27.7 -    val x = Term.variant used seed
    27.8 +    val x = Name.variant used seed
    27.9    in (x, x :: used) end;
   27.10  
   27.11  fun eta_expand (c as (_, (_, ty)), es) k =
    28.1 --- a/src/Pure/codegen.ML	Tue Jul 11 12:16:52 2006 +0200
    28.2 +++ b/src/Pure/codegen.ML	Tue Jul 11 12:16:54 2006 +0200
    28.3 @@ -337,7 +337,7 @@
    28.4  
    28.5  fun preprocess_term thy t =
    28.6    let
    28.7 -    val x = Free (variant (add_term_names (t, [])) "x", fastype_of t);
    28.8 +    val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
    28.9      (* fake definition *)
   28.10      val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
   28.11        (Logic.mk_equals (x, t));
   28.12 @@ -539,7 +539,7 @@
   28.13      val (illegal, alt_names) = split_list (map_filter (fn s =>
   28.14        let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
   28.15      val ps = (reserved @ illegal) ~~
   28.16 -      variantlist (map (suffix "'") reserved @ alt_names, names);
   28.17 +      Name.variant_list names (map (suffix "'") reserved @ alt_names);
   28.18  
   28.19      fun rename_id s = AList.lookup (op =) ps s |> the_default s;
   28.20  
   28.21 @@ -688,9 +688,9 @@
   28.22           separate (Pretty.brk 1) (p :: ps) @ [Pretty.str ")"])
   28.23       else Pretty.block (separate (Pretty.brk 1) (p :: ps));
   28.24  
   28.25 -fun new_names t xs = variantlist (map mk_id xs,
   28.26 -  map (fst o fst o dest_Var) (term_vars t) union
   28.27 -  add_term_names (t, ThmDatabase.ml_reserved));
   28.28 +fun new_names t xs = Name.variant_list
   28.29 +  (map (fst o fst o dest_Var) (term_vars t) union
   28.30 +    add_term_names (t, ThmDatabase.ml_reserved)) (map mk_id xs);
   28.31  
   28.32  fun new_name t x = hd (new_names t [x]);
   28.33  
    29.1 --- a/src/Pure/proofterm.ML	Tue Jul 11 12:16:52 2006 +0200
    29.2 +++ b/src/Pure/proofterm.ML	Tue Jul 11 12:16:54 2006 +0200
    29.3 @@ -568,8 +568,8 @@
    29.4              (([], [], [], []), prf);
    29.5      val fs' = map (fst o dest_Free) fs;
    29.6      val vs' = map (fst o dest_Var) vs;
    29.7 -    val names = vs' ~~ variantlist (map fst vs', fs');
    29.8 -    val names' = Tvs ~~ variantlist (map fst Tvs, Tfs);
    29.9 +    val names = vs' ~~ Name.variant_list fs' (map fst vs');
   29.10 +    val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs);
   29.11      val rnames = map swap names;
   29.12      val rnames' = map swap names';
   29.13    in
   29.14 @@ -607,7 +607,7 @@
   29.15      val fs = Term.fold_types (Term.fold_atyps
   29.16        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
   29.17      val ixns = add_term_tvar_ixns (t, []);
   29.18 -    val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
   29.19 +    val fmap = fs ~~ Name.variant_list (map #1 ixns) (map fst fs)
   29.20      fun thaw (f as (a, S)) =
   29.21        (case AList.lookup (op =) fmap f of
   29.22          NONE => TFree f
   29.23 @@ -619,7 +619,7 @@
   29.24  local
   29.25  
   29.26  fun new_name (ix, (pairs,used)) =
   29.27 -  let val v = variant used (string_of_indexname ix)
   29.28 +  let val v = Name.variant used (string_of_indexname ix)
   29.29    in  ((ix, v) :: pairs, v :: used)  end;
   29.30  
   29.31  fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
    30.1 --- a/src/Pure/pure_thy.ML	Tue Jul 11 12:16:52 2006 +0200
    30.2 +++ b/src/Pure/pure_thy.ML	Tue Jul 11 12:16:54 2006 +0200
    30.3 @@ -441,7 +441,7 @@
    30.4        (fn Var ((x, j), _) => if i = j then curry (op ins_string) x else I | _ => I);
    30.5      val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
    30.6      val vars = strip_vars prop;
    30.7 -    val cvars = (Term.variantlist (map #1 vars, used), vars)
    30.8 +    val cvars = (Name.variant_list used (map #1 vars), vars)
    30.9        |> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T)));
   30.10    in fold Thm.forall_elim cvars th end;
   30.11  
    31.1 --- a/src/Pure/thm.ML	Tue Jul 11 12:16:52 2006 +0200
    31.2 +++ b/src/Pure/thm.ML	Tue Jul 11 12:16:54 2006 +0200
    31.3 @@ -1343,7 +1343,7 @@
    31.4      val short = length iparams - length cs;
    31.5      val newnames =
    31.6        if short < 0 then error "More names than abstractions!"
    31.7 -      else variantlist (Library.take (short, iparams), cs) @ cs;
    31.8 +      else Name.variant_list cs (Library.take (short, iparams)) @ cs;
    31.9      val freenames = map (#1 o dest_Free) (term_frees Bi);
   31.10      val newBi = Logic.list_rename_params (newnames, Bi);
   31.11    in
    32.1 --- a/src/Pure/type.ML	Tue Jul 11 12:16:52 2006 +0200
    32.2 +++ b/src/Pure/type.ML	Tue Jul 11 12:16:54 2006 +0200
    32.3 @@ -233,7 +233,7 @@
    32.4      val fs = Term.fold_types (Term.fold_atyps
    32.5        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    32.6      val ixns = add_term_tvar_ixns (t, []);
    32.7 -    val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
    32.8 +    val fmap = fs ~~ map (rpair 0) (Name.variant_list (map #1 ixns) (map fst fs))
    32.9      fun thaw (f as (a, S)) =
   32.10        (case AList.lookup (op =) fmap f of
   32.11          NONE => TFree f
   32.12 @@ -246,7 +246,7 @@
   32.13  local
   32.14  
   32.15  fun new_name (ix, (pairs, used)) =
   32.16 -  let val v = variant used (string_of_indexname ix)
   32.17 +  let val v = Name.variant used (string_of_indexname ix)
   32.18    in ((ix, v) :: pairs, v :: used) end;
   32.19  
   32.20  fun freeze_one alist (ix, sort) =
    33.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Jul 11 12:16:52 2006 +0200
    33.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Jul 11 12:16:54 2006 +0200
    33.3 @@ -100,7 +100,7 @@
    33.4                 Sign.string_of_term sign t);
    33.5  
    33.6    (*** Construct the fixedpoint definition ***)
    33.7 -  val mk_variant = variant (foldr add_term_names [] intr_tms);
    33.8 +  val mk_variant = Name.variant (foldr add_term_names [] intr_tms);
    33.9  
   33.10    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   33.11  
    34.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Jul 11 12:16:52 2006 +0200
    34.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Jul 11 12:16:54 2006 +0200
    34.3 @@ -147,7 +147,7 @@
    34.4      (** make definition **)
    34.5  
    34.6      (*the recursive argument*)
    34.7 -    val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
    34.8 +    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
    34.9                          Ind_Syntax.iT)
   34.10  
   34.11      val def_tm = Logic.mk_equals