author wenzelm Mon, 16 Sep 2013 17:42:05 +0200 changeset 53669 6ede465b5be8 parent 53668 2da931497d2c child 53670 5ccee1cb245a
more antiquotations -- avoid unchecked string literals;
```--- 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 =```