fully qualified names: Theory.add_XXX;
authorwenzelm
Thu Oct 02 22:54:00 1997 +0200 (1997-10-02)
changeset 3771ede66fb99880
parent 3770 294b5905f4eb
child 3772 6ee707a73248
fully qualified names: Theory.add_XXX;
src/Cube/Cube.ML
src/HOLCF/ax_ops/thy_axioms.ML
src/HOLCF/ax_ops/thy_ops.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/syntax.ML
     1.1 --- a/src/Cube/Cube.ML	Wed Oct 01 18:19:44 1997 +0200
     1.2 +++ b/src/Cube/Cube.ML	Thu Oct 02 22:54:00 1997 +0200
     1.3 @@ -12,11 +12,11 @@
     1.4  
     1.5  val L2_thy =
     1.6    Cube.thy
     1.7 -  |> add_axioms
     1.8 +  |> Theory.add_axioms
     1.9     [("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
    1.10      ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
    1.11       \  ==> Abs(A,f) : Prod(A,B)")]
    1.12 -  |> add_thyname "L2";
    1.13 +  |> Theory.add_name "L2";
    1.14  
    1.15  val lam_bs = get_axiom L2_thy "lam_bs";
    1.16  val pi_bs = get_axiom L2_thy "pi_bs";
    1.17 @@ -25,11 +25,11 @@
    1.18  
    1.19  val Lomega_thy =
    1.20    Cube.thy
    1.21 -  |> add_axioms
    1.22 +  |> Theory.add_axioms
    1.23     [("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
    1.24      ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
    1.25       \  ==> Abs(A,f) : Prod(A,B)")]
    1.26 -  |> add_thyname "Lomega";
    1.27 +  |> Theory.add_name "Lomega";
    1.28  
    1.29  val lam_bb = get_axiom Lomega_thy "lam_bb";
    1.30  val pi_bb = get_axiom Lomega_thy "pi_bb";
    1.31 @@ -40,11 +40,11 @@
    1.32  
    1.33  val LP_thy =
    1.34    Cube.thy
    1.35 -  |> add_axioms
    1.36 +  |> Theory.add_axioms
    1.37     [("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
    1.38      ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
    1.39       \  ==> Abs(A,f) : Prod(A,B)")]
    1.40 -  |> add_thyname "LP";
    1.41 +  |> Theory.add_name "LP";
    1.42  
    1.43  val lam_sb = get_axiom LP_thy "lam_sb";
    1.44  val pi_sb = get_axiom LP_thy "pi_sb";
     2.1 --- a/src/HOLCF/ax_ops/thy_axioms.ML	Wed Oct 01 18:19:44 1997 +0200
     2.2 +++ b/src/HOLCF/ax_ops/thy_axioms.ML	Thu Oct 02 22:54:00 1997 +0200
     2.3 @@ -148,7 +148,7 @@
     2.4    let val {sign, ...} = rep_theory theory;
     2.5        val constraints = get_constraints_of_str sign (defvarlist@varlist)
     2.6    in
     2.7 -    add_axioms_i (map (apsnd 
     2.8 +    Theory.add_axioms_i (map (apsnd 
     2.9       (check_and_extend sign (map fst defvarlist) (map fst varlist)) o
    2.10                 (read_ext_axm sign constraints)) axioms) theory
    2.11    end 
    2.12 @@ -157,7 +157,7 @@
    2.13    let val {sign, ...} = rep_theory theory;
    2.14        val constraints = get_constraints_of_typ sign (defvarlist@varlist)
    2.15    in
    2.16 -    add_axioms_i (map (apsnd (check_and_extend sign 
    2.17 +    Theory.add_axioms_i (map (apsnd (check_and_extend sign 
    2.18                                 (map fst defvarlist) (map fst varlist)) o
    2.19                     (read_ext_axm_terms sign constraints)) axiom_terms) theory
    2.20    end
     3.1 --- a/src/HOLCF/ax_ops/thy_ops.ML	Wed Oct 01 18:19:44 1997 +0200
     3.2 +++ b/src/HOLCF/ax_ops/thy_ops.ML	Thu Oct 02 22:54:00 1997 +0200
     3.3 @@ -342,8 +342,8 @@
     3.4        val s_axms = (if strict then strictness_axms curried decls else []);
     3.5        val t_axms = (if total  then totality_axms   curried decls else []);
     3.6    in 
     3.7 -  add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) 
     3.8 -                     (add_syntax_i syndecls (add_consts_i oldstyledecls thy)))
     3.9 +  Theory.add_trrules_i xrules (Theory.add_axioms_i (s_axms @ t_axms) 
    3.10 +                     (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
    3.11    end;
    3.12  
    3.13  fun add_ops_i {curried,strict,total} decls thy =
    3.14 @@ -354,8 +354,8 @@
    3.15        val s_axms = (if strict then strictness_axms curried decls else []);
    3.16        val t_axms = (if total  then totality_axms   curried decls else []);
    3.17    in 
    3.18 -  add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) 
    3.19 -                     (add_syntax_i syndecls (add_consts_i oldstyledecls thy)))
    3.20 +  Theory.add_trrules_i xrules (Theory.add_axioms_i (s_axms @ t_axms) 
    3.21 +                     (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
    3.22    end;
    3.23  
    3.24  
     4.1 --- a/src/HOLCF/domain/axioms.ML	Wed Oct 01 18:19:44 1997 +0200
     4.2 +++ b/src/HOLCF/domain/axioms.ML	Thu Oct 02 22:54:00 1997 +0200
     4.3 @@ -123,7 +123,7 @@
     4.4      in foldr' mk_conj (mapn one_comp 0 eqs)end ));
     4.5    val thy_axs = flat (mapn (calc_axioms comp_dname eqs) 0 eqs) @
     4.6  		(if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def];
     4.7 -in thy' |> add_axioms_i (infer_types thy' thy_axs) end;
     4.8 +in thy' |> Theory.add_axioms_i (infer_types thy' thy_axs) end;
     4.9  
    4.10  
    4.11  fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let
    4.12 @@ -143,7 +143,7 @@
    4.13    val concl = mk_trp(foldr' mk_conj (map one_conc typs));
    4.14    val induct = (tname^"_induct",lift_adm(lift_pred_UU(
    4.15  			foldr (op ===>) (map one_cnstr cnstrs,concl))));
    4.16 -in thy' |> add_axioms_i (infer_types thy' [induct]) end;
    4.17 +in thy' |> Theory.add_axioms_i (infer_types thy' [induct]) end;
    4.18  
    4.19  end; (* local *)
    4.20  end; (* struct *)
     5.1 --- a/src/HOLCF/domain/syntax.ML	Wed Oct 01 18:19:44 1997 +0200
     5.2 +++ b/src/HOLCF/domain/syntax.ML	Thu Oct 02 22:54:00 1997 +0200
     5.3 @@ -115,11 +115,11 @@
     5.4    val const_bisim  = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
     5.5    val ctt           = map (calc_syntax funprod) eqs';
     5.6    val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
     5.7 -in thy'' |> add_types      thy_types
     5.8 -	 |> add_arities    thy_arities
     5.9 +in thy'' |> Theory.add_types      thy_types
    5.10 +	 |> Theory.add_arities    thy_arities
    5.11  	 |> add_cur_ops_i (flat(map fst ctt))
    5.12  	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
    5.13 -	 |> add_trrules_i (flat(map snd ctt))
    5.14 +	 |> Theory.add_trrules_i (flat(map snd ctt))
    5.15  end; (* let *)
    5.16  
    5.17  end; (* local *)