1.1 --- a/src/Tools/isac/Interpret/appl.sml Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -24,7 +24,7 @@
1.4 then
1.5 let
1.6 val thy' = get_obj g_domID pt p'
1.7 - val {rew_ord', erls, ...} = get_met (get_obj g_metID pt p')
1.8 + val {rew_ord', erls, ...} = Specify.get_met (get_obj g_metID pt p')
1.9 in ("OK", thy', rew_ord', erls, false) end
1.10 else
1.11 let
1.12 @@ -41,7 +41,7 @@
1.13 then
1.14 let
1.15 val thy' = get_obj g_domID pt p'
1.16 - val {calc = scr_isa_fns,...} = get_met (get_obj g_metID pt p')
1.17 + val {calc = scr_isa_fns,...} = Specify.get_met (get_obj g_metID pt p')
1.18 val opt = assoc (scr_isa_fns, scrop)
1.19 in
1.20 case opt of
1.21 @@ -224,7 +224,7 @@
1.22 else
1.23 let
1.24 val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
1.25 - val {ppc,...} = get_pbt pI'
1.26 + val {ppc,...} = Specify.get_pbt pI'
1.27 val pbl = Ctree.init_pbl ppc
1.28 in Chead.Appl (Model_Problem' (pI', pbl, [])) end
1.29
1.30 @@ -234,7 +234,7 @@
1.31 else
1.32 let
1.33 val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
1.34 - val opt = refine_ori oris pI;
1.35 + val opt = Specify.refine_ori oris pI;
1.36 in case opt of
1.37 SOME pblID =>
1.38 Chead.Appl (Refine_Tacitly' (pI, pblID,
1.39 @@ -250,12 +250,10 @@
1.40 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1.41 probl=itms, ...}) = get_obj I pt p;
1.42 val thy = if dI' = e_domID then dI else dI';
1.43 - val rfopt = refine_pbl (assoc_thy thy) pI itms;
1.44 + val rfopt = Specify.refine_pbl (assoc_thy thy) pI itms;
1.45 in case rfopt of
1.46 NONE => Chead.Notappl ((tac2str (Refine_Problem pI))^" not applicable")
1.47 | SOME (rf as (pI',_)) =>
1.48 -(* val SOME (rf as (pI',_)) = rfopt;
1.49 - *)
1.50 if pI' = pI
1.51 then Chead.Notappl ((tac2str (Refine_Problem pI))^" not applicable")
1.52 else Chead.Appl (Refine_Problem' rf)
1.53 @@ -316,10 +314,10 @@
1.54 let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
1.55 probl=itms, ...}) = get_obj I pt p;
1.56 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.57 - val {ppc,where_,prls,...} = get_pbt pID;
1.58 + val {ppc,where_,prls,...} = Specify.get_pbt pID;
1.59 val pbl = if pI'=e_pblID andalso pI=e_pblID
1.60 then (false, (Ctree.init_pbl ppc, []))
1.61 - else match_itms_oris thy itms (ppc,where_,prls) oris;
1.62 + else Specify.match_itms_oris thy itms (ppc,where_,prls) oris;
1.63 in Chead.Appl (Specify_Problem' (pID, pbl)) end
1.64 (* val Specify_Method mID = nxt; val (p,p_) = p;
1.65 *)
1.66 @@ -336,7 +334,7 @@
1.67 else
1.68 let
1.69 val (PblObj{origin = (_, (dI, pI, _), _), probl, ctxt, ...}) = get_obj I pt p;
1.70 - val {where_, ...} = get_pbt pI
1.71 + val {where_, ...} = Specify.get_pbt pI
1.72 val pres = map (mk_env probl |> subst_atomic) where_
1.73 val ctxt =
1.74 if is_e_ctxt ctxt
1.75 @@ -365,7 +363,7 @@
1.76 val pp = par_pblobj pt p;
1.77 val thy' = (get_obj g_domID pt pp): theory';
1.78 val thy = assoc_thy thy';
1.79 - val {rew_ord' = ro', erls = erls, ...} = get_met (get_obj g_metID pt pp);
1.80 + val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);
1.81 val (f, p) = case p_ of (*p 12.4.00 unnecessary*)
1.82 Frm => (get_obj g_form pt p, p)
1.83 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.84 @@ -409,8 +407,7 @@
1.85 val pp = par_pblobj pt p;
1.86 val thy' = (get_obj g_domID pt pp):theory';
1.87 val thy = assoc_thy thy';
1.88 - val {rew_ord'=ro',erls=erls,...} =
1.89 - get_met (get_obj g_metID pt pp);
1.90 + val {rew_ord'=ro',erls=erls,...} = Specify.get_met (get_obj g_metID pt pp);
1.91 (*val put_asm = true;*)
1.92 val (f, _) = case p_ of
1.93 Frm => (get_obj g_form pt p, p)
1.94 @@ -430,7 +427,7 @@
1.95 val pp = par_pblobj pt p;
1.96 val thy' = (get_obj g_domID pt pp):theory';
1.97 val thy = assoc_thy thy';
1.98 - val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
1.99 + val {rew_ord'=ro',...} = Specify.get_met (get_obj g_metID pt pp);
1.100 val f = case p_ of Frm => get_obj g_form pt p
1.101 | Res => (fst o (get_obj g_result pt)) p
1.102 | _ => error ("applicable_in: call by "^
1.103 @@ -452,8 +449,7 @@
1.104 val pp = par_pblobj pt p;
1.105 val thy' = (get_obj g_domID pt pp):theory';
1.106 val thy = assoc_thy thy';
1.107 - val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} =
1.108 - get_met (get_obj g_metID pt pp);
1.109 + val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} = Specify.get_met (get_obj g_metID pt pp);
1.110 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.111 Frm => (get_obj g_form pt p, p)
1.112 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.113 @@ -541,7 +537,7 @@
1.114 val f = case p_ of
1.115 Frm => get_obj g_form pt p
1.116 | Res => (fst o (get_obj g_result pt)) p
1.117 - val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
1.118 + val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp)
1.119 val subte = sube2subte sube
1.120 val subst = sube2subst thy sube
1.121 val ro = assoc_rew_ord rew_ord'
1.122 @@ -643,7 +639,7 @@
1.123 val thy' = (get_obj g_domID pt pp):theory';
1.124 val thy = assoc_thy thy'
1.125 val metID = (get_obj g_metID pt pp)
1.126 - val {crls,...} = get_met metID
1.127 + val {crls,...} = Specify.get_met metID
1.128 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
1.129 | Res => get_obj g_result pt p;
1.130 val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;