fully qualified names: Theory.add_XXX;
authorwenzelm
Wed Oct 01 18:13:41 1997 +0200 (1997-10-01)
changeset 376867f4ac759100
parent 3767 e2bb53d8dd26
child 3769 931c336b0707
fully qualified names: Theory.add_XXX;
TFL/tfl.sml
src/HOL/Inductive.ML
src/HOL/NatDef.ML
src/HOL/add_ind_def.ML
src/HOL/datatype.ML
src/HOL/typedef.ML
src/LCF/ex/ex.ML
src/ZF/add_ind_def.ML
     1.1 --- a/TFL/tfl.sml	Wed Oct 01 17:43:42 1997 +0200
     1.2 +++ b/TFL/tfl.sml	Wed Oct 01 18:13:41 1997 +0200
     1.3 @@ -338,7 +338,7 @@
     1.4  	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
     1.5  	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
     1.6  		propT)
     1.7 -  in  add_defs_i [(def_name, def_term)] thy  end
     1.8 +  in  Theory.add_defs_i [(def_name, def_term)] thy  end
     1.9  end;
    1.10  
    1.11  
    1.12 @@ -458,7 +458,7 @@
    1.13       val full_rqt = WFR::TCs
    1.14       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
    1.15       val R'abs = S.rand R'
    1.16 -     val theory = add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
    1.17 +     val theory = Theory.add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
    1.18  	                     thy
    1.19       val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
    1.20       val fconst = #lhs(S.dest_eq(concl def)) 
     2.1 --- a/src/HOL/Inductive.ML	Wed Oct 01 17:43:42 1997 +0200
     2.2 +++ b/src/HOL/Inductive.ML	Wed Oct 01 18:13:41 1997 +0200
     2.3 @@ -75,7 +75,7 @@
     2.4      val rec_tms = map (readtm sign termTVar) srec_tms
     2.5      and intr_tms = map (readtm sign propT) sintrs;
     2.6      val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms) 
     2.7 -                  |> add_thyname thy_name);
     2.8 +                  |> Theory.add_name thy_name);
     2.9  
    2.10  
    2.11  
     3.1 --- a/src/HOL/NatDef.ML	Wed Oct 01 17:43:42 1997 +0200
     3.2 +++ b/src/HOL/NatDef.ML	Wed Oct 01 18:13:41 1997 +0200
     3.3 @@ -724,6 +724,5 @@
     3.4  (* add function nat_add_primrec *) 
     3.5  val (_, nat_add_primrec, _) = Datatype.add_datatype
     3.6  ([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([],
     3.7 -"nat")], NoSyn)]) (add_thyname "Arith" HOL.thy);
     3.8 -(* pretend Arith is part of the basic theory to fool package *)
     3.9 -
    3.10 +"nat")], NoSyn)]) (Theory.add_name "Arith" HOL.thy);
    3.11 +(*pretend Arith is part of the basic theory to fool package*)
     4.1 --- a/src/HOL/add_ind_def.ML	Wed Oct 01 17:43:42 1997 +0200
     4.2 +++ b/src/HOL/add_ind_def.ML	Wed Oct 01 18:13:41 1997 +0200
     4.3 @@ -157,7 +157,7 @@
     4.4               | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^
     4.5                                 "\n\t*Consider adding type constraints*"))
     4.6  
     4.7 -  in  thy |> add_defs_i axpairs  end
     4.8 +  in  thy |> Theory.add_defs_i axpairs  end
     4.9  
    4.10  
    4.11  (****************************************************************OMITTED
    4.12 @@ -240,10 +240,6 @@
    4.13  *   val axpairs =
    4.14          big_case_def :: flat (ListPair.map mk_con_defs ((1 upto npart), con_ty_lists))
    4.15  
    4.16 -*   in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
    4.17 +*   in  thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs  end;
    4.18  ****************************************************************)
    4.19  end;
    4.20 -
    4.21 -
    4.22 -
    4.23 -
     5.1 --- a/src/HOL/datatype.ML	Wed Oct 01 17:43:42 1997 +0200
     5.2 +++ b/src/HOL/datatype.ML	Wed Oct 01 18:13:41 1997 +0200
     5.3 @@ -504,14 +504,14 @@
     5.4            val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
     5.5            val varT = Type.varifyT T;
     5.6            val ftyp = the (Sign.const_type sg fname);
     5.7 -        in add_defs_i [defpairT] thy end;
     5.8 +        in Theory.add_defs_i [defpairT] thy end;
     5.9  
    5.10      in
    5.11 -      (thy |> add_types types
    5.12 -           |> add_arities arities
    5.13 -           |> add_consts consts
    5.14 -           |> add_trrules xrules
    5.15 -           |> add_axioms rules, add_primrec, size_eqns)
    5.16 +      (thy |> Theory.add_types types
    5.17 +           |> Theory.add_arities arities
    5.18 +           |> Theory.add_consts consts
    5.19 +           |> Theory.add_trrules xrules
    5.20 +           |> Theory.add_axioms rules, add_primrec, size_eqns)
    5.21      end
    5.22  
    5.23  (*Warn if the (induction) variable occurs Free among the premises, which
     6.1 --- a/src/HOL/typedef.ML	Wed Oct 01 17:43:42 1997 +0200
     6.2 +++ b/src/HOL/typedef.ML	Wed Oct 01 18:13:41 1997 +0200
     6.3 @@ -107,17 +107,17 @@
     6.4      prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
     6.5  
     6.6      thy
     6.7 -    |> add_types [(t, tlen, mx)]
     6.8 -    |> add_arities
     6.9 +    |> Theory.add_types [(t, tlen, mx)]
    6.10 +    |> Theory.add_arities
    6.11       [(tname, replicate tlen logicS, logicS),
    6.12        (tname, replicate tlen termS, termS)]
    6.13 -    |> add_consts_i
    6.14 +    |> Theory.add_consts_i
    6.15       [(name, setT, NoSyn),
    6.16        (Rep_name, newT --> oldT, NoSyn),
    6.17        (Abs_name, oldT --> newT, NoSyn)]
    6.18 -    |> add_defs_i
    6.19 +    |> Theory.add_defs_i
    6.20       [(name ^ "_def", mk_equals (setC, set))]
    6.21 -    |> add_axioms_i
    6.22 +    |> Theory.add_axioms_i
    6.23       [(Rep_name, rep_type),
    6.24        (Rep_name ^ "_inverse", rep_type_inv),
    6.25        (Abs_name ^ "_inverse", abs_type_inv)]
     7.1 --- a/src/LCF/ex/ex.ML	Wed Oct 01 17:43:42 1997 +0200
     7.2 +++ b/src/LCF/ex/ex.ML	Wed Oct 01 18:13:41 1997 +0200
     7.3 @@ -11,16 +11,16 @@
     7.4  
     7.5  val ex_thy =
     7.6    thy
     7.7 -  |> add_consts
     7.8 +  |> Theory.add_consts
     7.9     [("P", "'a => tr", NoSyn),
    7.10      ("G", "'a => 'a", NoSyn),
    7.11      ("H", "'a => 'a", NoSyn),
    7.12      ("K", "('a => 'a) => ('a => 'a)", NoSyn)]
    7.13 -  |> add_axioms
    7.14 +  |> Theory.add_axioms
    7.15     [("P_strict", "P(UU) = UU"),
    7.16      ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
    7.17      ("H", "H = FIX(K)")]
    7.18 -  |> add_thyname "Ex 10.4";
    7.19 +  |> Theory.add_name "Ex 10.4";
    7.20  
    7.21  val ax = get_axiom ex_thy;
    7.22  
    7.23 @@ -55,17 +55,17 @@
    7.24  
    7.25  val ex_thy =
    7.26    thy
    7.27 -  |> add_consts
    7.28 +  |> Theory.add_consts
    7.29     [("P", "'a => tr", NoSyn),
    7.30      ("F", "'a => 'a", NoSyn),
    7.31      ("G", "'a => 'a", NoSyn),
    7.32      ("H", "'a => 'b => 'b", NoSyn),
    7.33      ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)]
    7.34 -  |> add_axioms
    7.35 +  |> Theory.add_axioms
    7.36     [("F_strict", "F(UU) = UU"),
    7.37      ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
    7.38      ("H", "H = FIX(K)")]
    7.39 -  |> add_thyname "Ex 3.8";
    7.40 +  |> Theory.add_name "Ex 3.8";
    7.41  
    7.42  val ax = get_axiom ex_thy;
    7.43  
    7.44 @@ -87,13 +87,13 @@
    7.45  
    7.46  val ex_thy =
    7.47    thy
    7.48 -  |> add_consts
    7.49 +  |> Theory.add_consts
    7.50     [("s", "'a => 'a", NoSyn),
    7.51      ("p", "'a => 'a => 'a", NoSyn)]
    7.52 -  |> add_axioms
    7.53 +  |> Theory.add_axioms
    7.54     [("p_strict", "p(UU) = UU"),
    7.55      ("p_s", "p(s(x),y) = s(p(x,y))")]
    7.56 -  |> add_thyname "fix ex";
    7.57 +  |> Theory.add_name "fix ex";
    7.58  
    7.59  val ax = get_axiom ex_thy;
    7.60  
     8.1 --- a/src/ZF/add_ind_def.ML	Wed Oct 01 17:43:42 1997 +0200
     8.2 +++ b/src/ZF/add_ind_def.ML	Wed Oct 01 18:13:41 1997 +0200
     8.3 @@ -162,7 +162,7 @@
     8.4  
     8.5      val dummy = seq (writeln o Sign.string_of_term sign o #2) axpairs
     8.6    
     8.7 -  in  thy |> add_defs_i axpairs  end
     8.8 +  in  thy |> Theory.add_defs_i axpairs  end
     8.9  
    8.10  
    8.11  (*Expects the recursive sets to have been defined already.
    8.12 @@ -250,5 +250,5 @@
    8.13          big_case_def :: flat (ListPair.map mk_con_defs
    8.14  			      (1 upto npart, con_ty_lists))
    8.15  
    8.16 -    in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
    8.17 +    in  thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs  end;
    8.18  end;