1.1 --- a/src/Tools/isac/Interpret/appl.sml	Wed Oct 10 18:41:15 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Fri Oct 12 16:03:07 2012 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4       (mk_and (Free("a",bool)) (Free("b",bool)));
     1.5  val it = "a & b" : cterm*)
     1.6  
     1.7 -fun mk_and [] = HOLogic.true_const
     1.8 +fun mk_and [] = @{term True}
     1.9    | mk_and (t::[]) = t
    1.10    | mk_and (t::ts) = 
    1.11      let fun mk t' (t::[]) = op_and $ t' $ t