test/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 41924 7407ceef2aed
parent 41922 32d7766945fb
child 41969 a350b4ed575b
     1.1 --- a/test/Tools/isac/Interpret/script.sml	Fri Mar 04 11:45:02 2011 +0100
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Thu Mar 10 12:45:58 2011 +0100
     1.3 @@ -184,7 +184,7 @@
     1.4     TYPE
     1.5        ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
     1.6           [],
     1.7 -         [Const ("Trueprop", "bool => prop") $
     1.8 +         [Const ("HOL.Trueprop", "bool => prop") $
     1.9                 (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
    1.10     raised
    1.11  ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"