src/Tools/isac/Interpret/solve.sml
branchdecompose-isar
changeset 41968 3228aa46fd30
parent 41960 3048fe25fe67
child 41972 22c5483e9bfb
     1.1 --- a/src/Tools/isac/Interpret/solve.sml	Sun May 01 17:16:57 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Tue May 03 11:16:55 2011 +0200
     1.3 @@ -1,8 +1,8 @@
     1.4 -(* solve an example by interpreting a method's script
     1.5 -   (c) Walther Neuper 1999
     1.6 -
     1.7 -use"ME/solve.sml";
     1.8 -use"solve.sml";
     1.9 +(* Title:  solve an example by interpreting a method's script
    1.10 +   Author: Walther Neuper 1999
    1.11 +   (c) copyright due to lincense terms.
    1.12 +1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
    1.13 +        10        20        30        40        50        60        70        80         90      100
    1.14  *)
    1.15  
    1.16  fun safe (ScrState (_,_,_,_,s,_)) = s
    1.17 @@ -142,10 +142,9 @@
    1.18  (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
    1.19     val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
    1.20     *)
    1.21 -fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) 
    1.22 -	  (pt:ptree, (pos as (p,_))) =
    1.23 -  let val {srls,...} = get_met mI;
    1.24 -    val PblObj{meth=itms,...} = get_obj I pt p;
    1.25 +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
    1.26 +  let val {srls, ...} = get_met mI;
    1.27 +    val PblObj {meth=itms, ...} = get_obj I pt p;
    1.28      val thy' = get_obj g_domID pt p;
    1.29      val thy = assoc_thy thy';
    1.30      val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;