# HG changeset patch
# User wenzelm
# Date 1379346125 -7200
# Node ID 6ede465b5be8e39f5787384d5ae94928ee3f9239
# Parent  2da931497d2c67923158de3d1208ac36ffb9537a
more antiquotations -- avoid unchecked string literals;

diff -r 2da931497d2c -r 6ede465b5be8 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 17:18:56 2013 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 17:42:05 2013 +0200
@@ -24,20 +24,20 @@
 open Function_Lib
 open Function_Common
 
-(* Extracts a function and its arguments from a proposition that is
+(* Extract a function and its arguments from a proposition that is
    either of the form "f x y z = ..." or, in case of function that
    returns a boolean, "f x y z" *)
-fun dest_funprop (Const ("HOL.eq", _) $ lhs $ rhs) = (strip_comb lhs, rhs)
-  | dest_funprop (Const ("HOL.Not", _) $ trm) = (strip_comb trm, @{term "False"})
+fun dest_funprop (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = (strip_comb lhs, rhs)
+  | dest_funprop (Const (@{const_name Not}, _) $ trm) = (strip_comb trm, @{term "False"})
   | dest_funprop trm = (strip_comb trm, @{term "True"});
 
 local
 
 fun propagate_tac i thm =
   let fun inspect eq = case eq of
-              Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ Free x $ t) =>
+              Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
                   if Logic.occs (Free x, t) then raise Match else true
-            | Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ t $ Free x) =>
+            | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
                   if Logic.occs (Free x, t) then raise Match else false
             | _ => raise Match;
       fun mk_eq thm = (if inspect (prop_of thm) then
@@ -87,7 +87,7 @@
                 let val y = Free("y",T) in
                   (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T)
                 end
-              | mk_funeq n (Type("fun",[S,T])) (acc_vars, acc_lhs) =
+              | mk_funeq n (Type(@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
                 let val xn = Free ("x" ^ Int.toString n,S) in
                   mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn)
                 end
@@ -133,7 +133,7 @@
                 |> Thm.forall_intr (cterm_of thy rhs_var)
 
           val bool_elims = (case ranT of
-                              Type ("HOL.bool", []) => mk_bool_elims ctxt elim_stripped
+                              Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
                               | _ => []);
 
           fun unstrip rl =