--- a/src/HOL/Decision_Procs/langford.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Thu Aug 19 11:02:14 2010 +0200
@@ -30,7 +30,7 @@
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
case term_of ep of
- Const("Ex",_)$_ =>
+ Const(@{const_name "Ex"},_)$_ =>
let
val p = Thm.dest_arg ep
val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
@@ -116,13 +116,13 @@
fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
fun is_eqx x eq = case term_of eq of
- Const("op =",_)$l$r => l aconv term_of x orelse r aconv term_of x
+ Const(@{const_name "op ="},_)$l$r => l aconv term_of x orelse r aconv term_of x
| _ => false ;
local
fun proc ct =
case term_of ct of
- Const("Ex",_)$Abs (xn,_,_) =>
+ Const(@{const_name "Ex"},_)$Abs (xn,_,_) =>
let
val e = Thm.dest_fun ct
val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
@@ -176,19 +176,19 @@
let
fun h bounds tm =
(case term_of tm of
- Const ("op =", T) $ _ $ _ =>
+ Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
- | Const ("Not", _) $ _ => h bounds (Thm.dest_arg tm)
- | Const ("All", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("Ex", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("op &", _) $ _ $ _ => find_args bounds tm
- | Const ("op |", _) $ _ $ _ => find_args bounds tm
- | Const ("op -->", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
- | Const ("Trueprop", _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))