1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Sun Jul 18 21:19:25 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jul 19 15:34:54 2021 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4  
     1.5  (*. evaluate the predicate matches (match on whole term only) .*)
     1.6  (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
     1.7 -fun eval_matches (_:string) "Prog_Expr.matches" (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy = 
     1.8 +fun eval_matches (_:string) "Prog_Expr.matches" (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) thy = 
     1.9      if TermC.matches thy tst pat
    1.10      then 
    1.11        let
    1.12 @@ -204,7 +204,7 @@
    1.13  
    1.14  (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
    1.15  fun eval_matchsub (_:string) "Prog_Expr.matchsub"
    1.16 -      (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy = 
    1.17 +      (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) thy = 
    1.18      if matchsub thy tst pat
    1.19      then 
    1.20        let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
    1.21 @@ -227,7 +227,7 @@
    1.22  fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
    1.23    | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
    1.24  (*("lhs"    ,("Prog_Expr.lhs"    , eval_lhs "")):calc*)
    1.25 -fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ = 
    1.26 +fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ = 
    1.27      SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
    1.28  	  HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
    1.29    | eval_lhs _ _ _ _ = NONE;
    1.30 @@ -242,7 +242,7 @@
    1.31  fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
    1.32    | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
    1.33  (*("rhs"    ,("Prog_Expr.rhs"    , eval_rhs "")):calc*)
    1.34 -fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ = 
    1.35 +fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ = 
    1.36      SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
    1.37  	  HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
    1.38    | eval_rhs _ _ _ _ = NONE;
    1.39 @@ -252,7 +252,7 @@
    1.40  fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
    1.41  
    1.42  (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
    1.43 -fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const ("Prog_Expr.occurs_in",_) $ v $ t)) _ =
    1.44 +fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
    1.45      ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
    1.46       tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*)
    1.47       if occurs_in v t
    1.48 @@ -270,7 +270,7 @@
    1.49  (*("some_occur_in", ("Prog_Expr.some_occur_in", 
    1.50  			eval_some_occur_in "#eval_some_occur_in_"))*)
    1.51  fun eval_some_occur_in _ "Prog_Expr.some_occur_in"
    1.52 -			  (p as (Const ("Prog_Expr.some_occur_in",_) $ vs $ t)) _ =
    1.53 +			  (p as (Const (\<^const_name>\<open>some_occur_in\<close>,_) $ vs $ t)) _ =
    1.54      if some_occur_in (TermC.isalist2list vs) t
    1.55      then SOME ((UnparseC.term p) ^ " = True",
    1.56  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.57 @@ -305,14 +305,14 @@
    1.58    | eval_is_even _ _ _ _ = NONE; 
    1.59  
    1.60  (*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
    1.61 -fun eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const ("Partial_Fractions.AA", _))) _ =
    1.62 +fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
    1.63      (*TODO get rid of this special case*)
    1.64      SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    1.65        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.66 -  | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const _)) _ =
    1.67 +  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
    1.68      SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    1.69        HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.70 -  | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ n)) _ =
    1.71 +  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
    1.72  	   if TermC.is_num n
    1.73  	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
    1.74         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))