1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -180,14 +180,14 @@
     1.4  > eval_matches "/thmid/" "/op_/" t thy;
     1.5  SOME
     1.6      ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
     1.7 -     Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
     1.8 +     Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
     1.9    : (string * term) option 
    1.10  
    1.11  > val t = (Thm.term_of o the o (parse thy)) 
    1.12  	      "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
    1.13  > eval_matches "/thmid/" "/op_/" t thy;
    1.14  SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
    1.15 -     Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
    1.16 +     Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
    1.17  
    1.18  > val t = (Thm.term_of o the o (parse thy)) 
    1.19                 "matches (a = b) (x + #1 + #-1 * #2 = #0)";
    1.20 @@ -334,10 +334,10 @@
    1.21     *)
    1.22  fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
    1.23    thmid ^ "Float ((" ^ 
    1.24 -  (string_of_int v11)^","^(string_of_int v12)^"), ("^
    1.25 -  (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
    1.26 -  (string_of_int v21)^","^(string_of_int v22)^"), ("^
    1.27 -  (string_of_int p21)^","^(string_of_int p22)^"))";
    1.28 +  (string_of_int v11)^", "^(string_of_int v12)^"), ("^
    1.29 +  (string_of_int p11)^", "^(string_of_int p12)^")) __ (("^
    1.30 +  (string_of_int v21)^", "^(string_of_int v22)^"), ("^
    1.31 +  (string_of_int p21)^", "^(string_of_int p22)^"))";
    1.32  
    1.33  (*.evaluate < and <= for numerals.*)
    1.34  (*("le"      ,("Orderings.ord_class.less"        , Prog_Expr.eval_equ "#less_")),