1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Apr 25 12:03:49 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Apr 25 12:49:37 2021 +0200
     1.3 @@ -170,7 +170,7 @@
     1.4       Const (#,#) $ (# $ # $ Const #)) : (string * term) option                  
     1.5  ----- before ?patterns ---:
     1.6  > val t  = (Thm.term_of o the o (parse thy)) 
     1.7 -	      "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
     1.8 +	      "matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1)";
     1.9  > eval_matches "/thmid/" "/op_/" t thy;
    1.10  SOME
    1.11      ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1) = True",
    1.12 @@ -178,7 +178,7 @@
    1.13    : (string * term) option 
    1.14  
    1.15  > val t = (Thm.term_of o the o (parse thy)) 
    1.16 -	      "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
    1.17 +	      "matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1)";
    1.18  > eval_matches "/thmid/" "/op_/" t thy;
    1.19  SOME ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1) = False",
    1.20       Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))