1.1 --- a/test/Tools/isac/Test_Isac.thy Mon Jul 18 15:20:40 2011 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Jul 18 15:29:25 2011 +0200
1.3 @@ -175,7 +175,7 @@
1.4 val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
1.5 autoord auto < 5 (*false*);
1.6 (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
1.7 -"~~~~~ fun all_modspec, args:"; val (pt, (p,_)) = (ptp');
1.8 +"~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
1.9 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
1.10 val thy = assoc_thy dI;
1.11 val {ppc, ...} = get_met mI;
1.12 @@ -184,8 +184,10 @@
1.13 (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]); *)
1.14 (*vvv from: | assod pt _ (Subproblem'...*)
1.15 val (fmz_, vals) = oris2fmz_vals pors;
1.16 - val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global
1.17 + (*
1.18 + val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global
1.19 |> declare_constraints' vals
1.20 +*)
1.21 (*^^^ from: | assod pt _ (Subproblem'...*)
1.22 val [(1, [1], "#Given", dsc_eq, [equality]),
1.23 (2, [1], "#Given", dsc_solvefor, [xxx]),
1.24 @@ -195,6 +197,20 @@
1.25 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.26 val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
1.27 val pt = update_spec pt p (dI,pI,mI);
1.28 +*}
1.29 +ML {*
1.30 +p;
1.31 +pos;
1.32 + get_assumptions_ pt pos |> terms2strs;
1.33 +tac_;
1.34 +*}
1.35 +ML {*
1.36 +print_depth 999; Subproblem'; print_depth 999;
1.37 +*}
1.38 +ML {*
1.39 +print_depth 999; tac_; print_depth 999;
1.40 +*}
1.41 +ML {*
1.42 val pt = update_ctxt pt p ctxt;
1.43 "~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
1.44 case complete_solve auto (c @ c') ptp of