1.1 --- a/src/Tools/isac/ME/ctree.sml Thu Aug 19 12:00:46 2010 +0200
1.2 +++ b/src/Tools/isac/ME/ctree.sml Thu Aug 19 12:08:42 2010 +0200
1.3 @@ -233,10 +233,10 @@
1.4 (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o
1.5 (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*)
1.6 fun subst2subs s = map (pair2str o
1.7 - (apfst (Syntax.string_of_term (ctxt_Isac""))) o
1.8 - (apsnd (Syntax.string_of_term (ctxt_Isac"")))) s;
1.9 -fun subst2subs' s = map ((apfst (Syntax.string_of_term (ctxt_Isac""))) o
1.10 - (apsnd (Syntax.string_of_term (ctxt_Isac"")))) s;
1.11 + (apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o
1.12 + (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s;
1.13 +fun subst2subs' s = map ((apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o
1.14 + (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s;
1.15 fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
1.16 (*> subs2subst thy ["(bdv,x)","(err,#0)"];
1.17 val it =
1.18 @@ -679,8 +679,8 @@
1.19 "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
1.20 | Rewrite_Set'(thy',pasm,rls',f,(f',asm))
1.21 => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","
1.22 - ^(Syntax.string_of_term (ctxt_Isac"") f)^",("^(Syntax.string_of_term (ctxt_Isac"") f')
1.23 - ^","^((strs2str o (map (Syntax.string_of_term (ctxt_Isac"")))) asm)^"))"
1.24 + ^(Syntax.string_of_term (thy2ctxt' "Isac") f)^",("^(Syntax.string_of_term (thy2ctxt' "Isac") f')
1.25 + ^","^((strs2str o (map (Syntax.string_of_term (thy2ctxt' "Isac")))) asm)^"))"
1.26
1.27 | End_Detail' _ => "End_Detail' xxx"
1.28 | Detail_Set' _ => "Detail_Set' xxx"
1.29 @@ -724,8 +724,8 @@
1.30 "\n("^(loc_2str l)^",("^(tac_2str m)^
1.31 ",\n ens= "^(subst2str eno)^
1.32 ",\n env= "^(subst2str env)^
1.33 - ",\n iar= "^(Syntax.string_of_term (ctxt_Isac"") iar)^
1.34 - ",\n res= "^(Syntax.string_of_term (ctxt_Isac"") res)^
1.35 + ",\n iar= "^(Syntax.string_of_term (thy2ctxt' "Isac") iar)^
1.36 + ",\n res= "^(Syntax.string_of_term (thy2ctxt' "Isac") res)^
1.37 ",\n "^(safe2str s)^"))";
1.38 fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;
1.39
1.40 @@ -852,16 +852,16 @@
1.41 (* show hd origin or form only *)
1.42 fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) =
1.43 ((pr_pos p) ^ " ----- pblobj -----\n")
1.44 -(* ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^
1.45 - (((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^
1.46 +(* ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
1.47 + (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
1.48 "\n") *)
1.49 | pr_short p (PrfObj {form = form,...}) =
1.50 ((pr_pos p) ^ (term2str form) ^ "\n");
1.51 (*
1.52 fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) =
1.53 ((ints2str c) ^" "^
1.54 - ((((Syntax.string_of_term (ctxt_Isac"")) o #4 o hd) ori)^" "^
1.55 - (((Syntax.string_of_term (ctxt_Isac"")) o hd(*!?!*) o #5 o hd) ori))^
1.56 + ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^
1.57 + (((Syntax.string_of_term (thy2ctxt' "Isac")) o hd(*!?!*) o #5 o hd) ori))^
1.58 "\n")
1.59 | pr_cell p (PrfObj {cell = c, form = form,...}) =
1.60 ((ints2str c) ^" "^ (term2str form) ^ "\n");
2.1 --- a/src/Tools/isac/ME/mstools.sml Thu Aug 19 12:00:46 2010 +0200
2.2 +++ b/src/Tools/isac/ME/mstools.sml Thu Aug 19 12:08:42 2010 +0200
2.3 @@ -643,7 +643,7 @@
2.4 | [t] => (case t of (*eg. eps=#0*)
2.5 (Const ("op =",_) $ l $ r) => [r,l]
2.6 | _ => raise error ("pbl_ids' Tools.nam: no equality "
2.7 - ^(Syntax.string_of_term (ctxt_Isac"")t)))
2.8 + ^(Syntax.string_of_term (thy2ctxt' "Isac")t)))
2.9 | vs' => vs (*14.9.01: ???TODO *))
2.10 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs
2.11 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs
3.1 --- a/src/Tools/isac/ME/ptyps.sml Thu Aug 19 12:00:46 2010 +0200
3.2 +++ b/src/Tools/isac/ME/ptyps.sml Thu Aug 19 12:08:42 2010 +0200
3.3 @@ -15,16 +15,16 @@
3.4 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
3.5
3.6 fun itm_2item thy (Cor ((d,ts),_)) =
3.7 - Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
3.8 + Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
3.9 | itm_2item _ (Syn c) = SyntaxE c
3.10 | itm_2item _ (Typ c) = TypeE c
3.11 | itm_2item thy (Inc ((d,ts),_)) =
3.12 - Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
3.13 + Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
3.14 | itm_2item thy (Sup (d,ts)) =
3.15 - Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
3.16 + Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
3.17 | itm_2item _ (Mis (d,pid)) =
3.18 - Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^
3.19 - Syntax.string_of_term (ctxt_Isac"") pid);
3.20 + Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^
3.21 + Syntax.string_of_term (thy2ctxt' "Isac") pid);
3.22
3.23
3.24 (* --- 8.3.00
3.25 @@ -99,7 +99,7 @@
3.26 else (e_term, [t]) (*??? 9.01 just copied*)
3.27 end)
3.28 handle _ => raise error ("split_dsc: called with "^
3.29 - (Syntax.string_of_term (ctxt_Isac"") t));
3.30 + (Syntax.string_of_term (thy2ctxt' "Isac") t));
3.31 (*
3.32 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
3.33 > split_dsc t1;
3.34 @@ -134,14 +134,14 @@
3.35
3.36
3.37 (*create output-string for itm_*)
3.38 -fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
3.39 +fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
3.40 | itm_out thy (Syn c) = c
3.41 | itm_out thy (Typ c) = c
3.42 - | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
3.43 - | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
3.44 + | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
3.45 + | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
3.46 | itm_out thy (Mis (d,pid)) =
3.47 - Syntax.string_of_term (ctxt_Isac"") d ^" "^
3.48 - Syntax.string_of_term (ctxt_Isac"") pid;
3.49 + Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^
3.50 + Syntax.string_of_term (thy2ctxt' "Isac") pid;
3.51
3.52 (*22.11.00 unused
3.53 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
3.54 @@ -163,15 +163,15 @@
3.55 *)
3.56 (*--3.3.00
3.57 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
3.58 - Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
3.59 + Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
3.60 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c
3.61 | itm2item (_,_,_,_,Typ (c)) = TypeE c
3.62 | itm2item (_,_,_,_,Fal (d,ts)) =
3.63 - False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
3.64 + False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
3.65 | itm2item (_,_,_,_,Inc (d,ts)) =
3.66 - Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
3.67 + Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
3.68 | itm2item (_,_,_,_,Sup (d,ts)) =
3.69 - Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)));
3.70 + Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)));
3.71 *)
3.72
3.73 fun boolterm2item (true, term) = Correct (term2str term)
3.74 @@ -199,7 +199,7 @@
3.75 then ("#Relate",d,ts)
3.76 else ("#undef",d,ts);
3.77 (* 28.1.00 raise error ("add_field: '"^
3.78 - (Syntax.string_of_term (ctxt_Isac"") d)^
3.79 + (Syntax.string_of_term (thy2ctxt' "Isac") d)^
3.80 "' not in ppc-description "); *)
3.81 ------9.3. *)
3.82
3.83 @@ -211,7 +211,7 @@
3.84 [(fi,(dsc,_))] => (fi,d,ts)
3.85 | [] => ("#undef",d,ts) (*may come with met.ppc*)
3.86 | _ => raise error ("add_field: "^
3.87 - (Syntax.string_of_term (ctxt_Isac"") d)^
3.88 + (Syntax.string_of_term (thy2ctxt' "Isac") d)^
3.89 " more than once in pbt")
3.90 end;
3.91
3.92 @@ -226,10 +226,10 @@
3.93 [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
3.94 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
3.95 (*raise error ("add_field': "^
3.96 - (Syntax.string_of_term (ctxt_Isac"") d)^
3.97 + (Syntax.string_of_term (thy2ctxt' "Isac") d)^
3.98 " not in met"*)
3.99 | _ => raise error ("add_field': "^
3.100 - (Syntax.string_of_term (ctxt_Isac"") d)^
3.101 + (Syntax.string_of_term (thy2ctxt' "Isac") d)^
3.102 " more than once in met");
3.103 in (flat ((map (repl mpc)) ori)):ori list end;
3.104
4.1 --- a/src/Tools/isac/Scripts/term_G.sml Thu Aug 19 12:00:46 2010 +0200
4.2 +++ b/src/Tools/isac/Scripts/term_G.sml Thu Aug 19 12:08:42 2010 +0200
4.3 @@ -714,7 +714,7 @@
4.4 fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm :
4.5 val it = fn : Theory.theory -> xstring -> Thm.thm*)
4.6 Thm (xstring,
4.7 - num_str (ProofContext.get_thm (ctxt_Isac"") xstring));
4.8 + num_str (ProofContext.get_thm (thy2ctxt' "Isac") xstring));
4.9
4.10 (** get types of Free and Abs for parse' **)
4.11 (*11.1.00: not used, fix-typed +,*,-,^ instead *)
5.1 --- a/src/Tools/isac/calcelems.sml Thu Aug 19 12:00:46 2010 +0200
5.2 +++ b/src/Tools/isac/calcelems.sml Thu Aug 19 12:08:42 2010 +0200
5.3 @@ -136,12 +136,13 @@
5.4
5.5 (*ctxt for retrieval of all thms in HOL; FIXME make this local?*)
5.6 (*val ctxt_HOL = ProofContext.init_global (theory "Complex_Main");*)
5.7 -val ctxt_HOL = thy2ctxt' "Complex_Main";
5.8 +(*val ctxt_HOL = thy2ctxt' "Complex_Main";*)
5.9 (*lazy ctxt for retrieval of all thms used in isac; FIXME make this local?*)
5.10 -fun ctxt_Isac _ = thy2ctxt' "Isac";
5.11 -fun Isac _ = ProofContext.theory_of (ctxt_Isac"");
5.12 +(*fun ctxt_Isac _ = thy2ctxt' "Isac";*)
5.13 +fun Isac _ = ProofContext.theory_of (thy2ctxt' "Isac");
5.14
5.15 -val e_rule = Thm ("refl", ProofContext.get_thm ctxt_HOL "refl" );
5.16 +val e_rule =
5.17 + Thm ("refl", ProofContext.get_thm (thy2ctxt' "Complex_Main") "refl" );
5.18 fun id_of_thm (Thm (id, _)) = id
5.19 | id_of_thm _ = raise error "id_of_thm";
5.20 fun thm_of_thm (Thm (_, thm)) = thm
5.21 @@ -599,13 +600,13 @@
5.22 "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)
5.23 | termopt2str NONE = "NONE";*)
5.24 fun termopt2str (SOME t) =
5.25 - "SOME " ^ (Syntax.string_of_term (ctxt_Isac"") t)
5.26 + "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
5.27 | termopt2str NONE = "NONE";
5.28 -fun term2str t = Syntax.string_of_term (ctxt_Isac"") t;
5.29 +fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t;
5.30 fun terms2str ts= (strs2str o (map (Syntax.string_of_term
5.31 - (ctxt_Isac"")))) ts;
5.32 + (thy2ctxt' "Isac")))) ts;
5.33 (*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*)
5.34 -fun type2str typ = Syntax.string_of_typ (ctxt_Isac"") typ;
5.35 +fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
5.36 val string_of_typ = type2str;
5.37
5.38 fun subst2str (s:subst) =