1.1 --- a/src/Tools/isac/ProgLang/Tools.thy	Fri Oct 08 18:58:24 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Tools.thy	Sat Oct 09 16:03:49 2010 +0200
     1.3 @@ -95,9 +95,11 @@
     1.4  		 (t as Const ("Tools.matches",_) $ pat $ tst) thy = 
     1.5      if matches thy tst pat
     1.6      then let val prop = Trueprop $ (mk_equality (t, true_as_term))
     1.7 -	 in SOME (Syntax.string_of_term @{context} prop, prop) end
     1.8 +	 in SOME (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) 
     1.9 +                                   prop, prop) end
    1.10      else let val prop = Trueprop $ (mk_equality (t, false_as_term))
    1.11 -	 in SOME (Syntax.string_of_term @{context} prop, prop) end
    1.12 +	 in SOME (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) 
    1.13 +                                   prop, prop) end
    1.14    | eval_matches _ _ _ _ = NONE; 
    1.15  (*
    1.16  > val t  = (term_of o the o (parse thy)) 
    1.17 @@ -170,9 +172,11 @@
    1.18  		 (t as Const ("Tools.matchsub",_) $ pat $ tst) thy = 
    1.19      if matchsub thy tst pat
    1.20      then let val prop = Trueprop $ (mk_equality (t, true_as_term))
    1.21 -	 in SOME (Syntax.string_of_term @{context} prop, prop) end
    1.22 +	 in SOME (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) 
    1.23 +                                   prop, prop) end
    1.24      else let val prop = Trueprop $ (mk_equality (t, false_as_term))
    1.25 -	 in SOME (Syntax.string_of_term @{context} prop, prop) end
    1.26 +	 in SOME (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) 
    1.27 +                                   prop, prop) end
    1.28    | eval_matchsub _ _ _ _ = NONE; 
    1.29  
    1.30  (*get the variables in an isabelle-term*)
    1.31 @@ -181,7 +185,8 @@
    1.32    (t as (Const(op0,t0) $ arg)) thy = 
    1.33    let 
    1.34      val t' = ((list2isalist HOLogic.realT) o vars) t;
    1.35 -    val thmId = thmid^(Syntax.string_of_term @{context} arg);
    1.36 +    val thmId = thmid ^ (Print_Mode.setmp [] (Syntax.string_of_term 
    1.37 +                                                     (thy2ctxt thy)) arg);
    1.38    in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.39    | eval_var _ _ _ _ = NONE;
    1.40