1.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Jul 18 09:50:15 2011 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Jul 18 15:29:14 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