1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Apr 13 13:13:07 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Apr 13 13:27:55 2020 +0200
     1.3 @@ -136,11 +136,11 @@
     1.4      then 
     1.5        let
     1.6          val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
     1.7 -	    in SOME (UnparseC.term_thy thy prop, prop) end
     1.8 +	    in SOME (UnparseC.term_in_thy thy prop, prop) end
     1.9      else 
    1.10        let 
    1.11          val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
    1.12 -	    in SOME (UnparseC.term_thy thy prop, prop) end
    1.13 +	    in SOME (UnparseC.term_in_thy thy prop, prop) end
    1.14    | eval_matches _ _ _ _ = NONE; 
    1.15  (*
    1.16  > val t  = (Thm.term_of o the o (parse thy)) 
    1.17 @@ -215,10 +215,10 @@
    1.18      if matchsub thy tst pat
    1.19      then 
    1.20        let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
    1.21 -      in SOME (UnparseC.term_thy thy prop, prop) end
    1.22 +      in SOME (UnparseC.term_in_thy thy prop, prop) end
    1.23      else 
    1.24        let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
    1.25 -      in SOME (UnparseC.term_thy thy prop, prop) end
    1.26 +      in SOME (UnparseC.term_in_thy thy prop, prop) end
    1.27    | eval_matchsub _ _ _ _ = NONE; 
    1.28  
    1.29  (*get the variables in an isabelle-term*)
    1.30 @@ -226,7 +226,7 @@
    1.31  fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy = 
    1.32      let 
    1.33        val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
    1.34 -      val thmId = thmid ^ UnparseC.term_thy thy arg;
    1.35 +      val thmId = thmid ^ UnparseC.term_in_thy thy arg;
    1.36      in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
    1.37    | eval_var _ _ _ _ = NONE;
    1.38  
    1.39 @@ -386,12 +386,12 @@
    1.40  	       (Const _(*op0, t0*) $ t1 $ t2 )) thy = 
    1.41    if t1 = t2
    1.42    then SOME (TermC.mk_thmid thmid 
    1.43 -	              ("(" ^ (UnparseC.term_thy thy t1) ^ ")")
    1.44 -	              ("(" ^ (UnparseC.term_thy thy t2) ^ ")"), 
    1.45 +	              ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
    1.46 +	              ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"), 
    1.47  	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.48    else SOME (TermC.mk_thmid thmid  
    1.49 -	              ("(" ^ (UnparseC.term_thy thy t1) ^ ")")
    1.50 -	              ("(" ^ (UnparseC.term_thy thy t2) ^ ")"),  
    1.51 +	              ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
    1.52 +	              ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),  
    1.53  	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.54    | eval_ident _ _ _ _ = NONE;
    1.55  (* TODO
    1.56 @@ -420,7 +420,7 @@
    1.57    if t1 = t2
    1.58    then
    1.59      SOME (TermC.mk_thmid thmid
    1.60 -      ("(" ^ UnparseC.term_thy thy t1 ^ ")") ("(" ^ UnparseC.term_thy thy t2 ^ ")"), 
    1.61 +      ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"), 
    1.62        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.63    else
    1.64      (case (TermC.is_atom t1, TermC.is_atom t2) of
    1.65 @@ -428,7 +428,7 @@
    1.66          if TermC.variable_constant_pair (t1, t2)
    1.67          then NONE
    1.68          else SOME (TermC.mk_thmid thmid
    1.69 -          ("(" ^ UnparseC.term_thy thy t1 ^ ")") ("(" ^ UnparseC.term_thy thy t2 ^ ")"),
    1.70 +          ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
    1.71            HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.72      | _ => NONE)                                              (* NOT is_atom t1,t2 --> rew_sub *)
    1.73    | eval_equal _ _ _ _ = NONE;                                                   (* error-exit *)