1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed Oct 10 18:41:15 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri Oct 12 16:03:07 2012 +0200
     1.3 @@ -710,7 +710,7 @@
     1.4  fun rep_tac_ (Rewrite_Inst' 
     1.5  		 (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) = 
     1.6    let val fT = type_of f;
     1.7 -    val b = if put then HOLogic.true_const else HOLogic.false_const;
     1.8 +    val b = if put then @{term True} else @{term False};
     1.9      val sT = (type_of o fst o hd) subs;
    1.10      val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
    1.11        (map HOLogic.mk_prod subs);
    1.12 @@ -752,7 +752,7 @@
    1.13  			      (map HOLogic.mk_prod subs);
    1.14  > val sT' = type_of subs';
    1.15  > val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT) 
    1.16 -  $ subs' $ Free (thmID,idT) $ HOLogic.true_const $ f;
    1.17 +  $ subs' $ Free (thmID,idT) $ @{term True} $ f;
    1.18  > lhs = tt;
    1.19  val it = true : bool
    1.20  > rep_tac_ (Rewrite_Inst' 
    1.21 @@ -762,7 +762,7 @@
    1.22    | rep_tac_ (Rewrite' (thy',rod,rls,put,(thmID,thm),f,(f',asm)))=
    1.23    let 
    1.24      val fT = type_of f;
    1.25 -    val b = if put then HOLogic.true_const else HOLogic.false_const;
    1.26 +    val b = if put then @{term True} else @{term False};
    1.27      val lhs = Const ("Script.Rewrite",[idT,HOLogic.boolT,fT] ---> fT)
    1.28        $ Free (thmID,idT) $ b $ f;
    1.29    in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
    1.30 @@ -790,7 +790,7 @@
    1.31      val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
    1.32        (map HOLogic.mk_prod subs);
    1.33      val sT' = type_of subs';
    1.34 -    val b = if put then HOLogic.true_const else HOLogic.false_const
    1.35 +    val b = if put then @{term True} else @{term False}
    1.36      val lhs = Const ("Script.Rewrite'_Set'_Inst",
    1.37  		     [sT',idT,fT,fT] ---> fT) 
    1.38        $ subs' $ Free (id_rls rls,idT) $ b $ f;
    1.39 @@ -804,7 +804,7 @@
    1.40  *)
    1.41    | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=
    1.42    let val fT = type_of f;
    1.43 -    val b = if put then HOLogic.true_const else HOLogic.false_const;
    1.44 +    val b = if put then @{term True} else @{term False};
    1.45      val lhs = Const ("Script.Rewrite'_Set",[idT,bool,fT] ---> fT) 
    1.46        $ Free (id_rls rls,idT) $ b $ f;
    1.47    in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end