1.1 --- a/src/Tools/isac/Interpret/solve.sml	Wed Dec 21 08:57:47 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Wed Dec 21 09:21:26 2016 +0100
     1.3 @@ -5,6 +5,10 @@
     1.4          10        20        30        40        50        60        70        80         90      100
     1.5  *)
     1.6  
     1.7 +structure Solve =
     1.8 +struct
     1.9 +(*open Ctree;*)
    1.10 +
    1.11  fun safe (ScrState (_,_,_,_,s,_)) = s
    1.12    | safe (RrlsState _) = Safe;
    1.13  
    1.14 @@ -73,7 +77,6 @@
    1.15  			    
    1.16  | Empty_Tac               => ("Empty_Tac",Empty_Tac)
    1.17  | Tac string              => ("Tac",Tac string)
    1.18 -| User                      => ("User",User)
    1.19  | End_Proof'                => ("End_Proof'",End_Proof'); 
    1.20  
    1.21  (*Detail*)
    1.22 @@ -131,7 +134,6 @@
    1.23  		 "Add_Relation","Del_Relation",
    1.24  		 "Specify_Theory","Specify_Problem","Specify_Method"];
    1.25  
    1.26 -"-----------------------------------------------------------------------";
    1.27  
    1.28  
    1.29  fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
    1.30 @@ -479,3 +481,4 @@
    1.31        else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
    1.32  	   in (*f*) Generate.EmptyMout end;
    1.33   
    1.34 +end
    1.35 \ No newline at end of file