src/Tools/isac/Interpret/mathengine.sml
branchdecompose-isar
changeset 42011 6a9ba30ab6bc
parent 42009 5f5807893ceb
child 42067 9f1489c78cb9
     1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Fri May 20 07:24:18 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Fri May 20 08:12:51 2011 +0200
     1.3 @@ -377,13 +377,11 @@
     1.4  (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
     1.5     compare "fun CalcTree" which DOES decode.*)
     1.6  fun CalcTreeTEST [(fmz, sp):fmz] = 
     1.7 -(* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
     1.8 -   val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
     1.9 -   *)
    1.10 -    let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
    1.11 -	val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
    1.12 -	val f = TESTg_form (pt,p)
    1.13 -    in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end; 
    1.14 +  let
    1.15 +    val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
    1.16 +	  val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
    1.17 +	  val f = TESTg_form (pt,p)
    1.18 +  in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end; 
    1.19         
    1.20  (*for tests > 15.8.03 after separation setnexttactic / nextTac:
    1.21    external view: me should be used by math-authors as done so far