# HG changeset patch
# User haftmann
# Date 1282226581 -7200
# Node ID f8999e19dd49541c63f0758f3e101a40816e22e8
# Parent  56965d8e4e1178c94ac3e206b6f754710922a98e
corrected some long-overseen misperceptions in recdef

diff -r 56965d8e4e11 -r f8999e19dd49 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Recdef.thy	Thu Aug 19 16:03:01 2010 +0200
@@ -5,7 +5,7 @@
 header {* TFL: recursive function definitions *}
 
 theory Recdef
-imports FunDef Plain
+imports Plain Hilbert_Choice
 uses
   ("Tools/TFL/casesplit.ML")
   ("Tools/TFL/utils.ML")
diff -r 56965d8e4e11 -r f8999e19dd49 src/HOL/Tools/TFL/dcterm.ML
--- a/src/HOL/Tools/TFL/dcterm.ML	Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML	Thu Aug 19 16:03:01 2010 +0200
@@ -24,18 +24,15 @@
   val dest_exists: cterm -> cterm * cterm
   val dest_forall: cterm -> cterm * cterm
   val dest_imp: cterm -> cterm * cterm
-  val dest_let: cterm -> cterm * cterm
   val dest_neg: cterm -> cterm
   val dest_pair: cterm -> cterm * cterm
   val dest_var: cterm -> {Name:string, Ty:typ}
   val is_conj: cterm -> bool
-  val is_cons: cterm -> bool
   val is_disj: cterm -> bool
   val is_eq: cterm -> bool
   val is_exists: cterm -> bool
   val is_forall: cterm -> bool
   val is_imp: cterm -> bool
-  val is_let: cterm -> bool
   val is_neg: cterm -> bool
   val is_pair: cterm -> bool
   val list_mk_disj: cterm list -> cterm
@@ -78,15 +75,15 @@
 
 fun mk_exists (r as (Bvar, Body)) =
   let val ty = #T(rep_cterm Bvar)
-      val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
+      val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
   in capply c (uncurry cabs r) end;
 
 
-local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
 in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
 end;
 
-local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
 in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
 end;
 
@@ -128,17 +125,15 @@
   handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
 
 
-val dest_neg    = dest_monop "not"
-val dest_pair   = dest_binop @{const_name Pair};
-val dest_eq     = dest_binop "op ="
-val dest_imp    = dest_binop "op -->"
-val dest_conj   = dest_binop "op &"
-val dest_disj   = dest_binop "op |"
-val dest_cons   = dest_binop "Cons"
-val dest_let    = Library.swap o dest_binop "Let";
-val dest_select = dest_binder "Hilbert_Choice.Eps"
-val dest_exists = dest_binder "Ex"
-val dest_forall = dest_binder "All"
+val dest_neg    = dest_monop @{const_name Not}
+val dest_pair   = dest_binop @{const_name Pair}
+val dest_eq     = dest_binop @{const_name "op ="}
+val dest_imp    = dest_binop @{const_name "op -->"}
+val dest_conj   = dest_binop @{const_name "op &"}
+val dest_disj   = dest_binop @{const_name "op |"}
+val dest_select = dest_binder @{const_name Eps}
+val dest_exists = dest_binder @{const_name Ex}
+val dest_forall = dest_binder @{const_name All}
 
 (* Query routines *)
 
@@ -151,8 +146,6 @@
 val is_conj   = can dest_conj
 val is_disj   = can dest_disj
 val is_pair   = can dest_pair
-val is_let    = can dest_let
-val is_cons   = can dest_cons
 
 
 (*---------------------------------------------------------------------------
@@ -197,7 +190,7 @@
   handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
     | TERM (msg, _) => raise ERR "mk_prop" msg;
 
-fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm;
+fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle U.ERR _ => ctm;
 
 
 end;
diff -r 56965d8e4e11 -r f8999e19dd49 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Thu Aug 19 16:03:01 2010 +0200
@@ -453,14 +453,14 @@
 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
 fun is_cong thm =
   case (Thm.prop_of thm)
-     of (Const("==>",_)$(Const(@{const_name "Trueprop"},_)$ _) $
+     of (Const("==>",_)$(Const(@{const_name Trueprop},_)$ _) $
          (Const("==",_) $ (Const (@{const_name Recdef.cut},_) $ f $ R $ a $ x) $ _)) => false
       | _ => true;
 
 
 fun dest_equal(Const ("==",_) $
-               (Const (@{const_name "Trueprop"},_) $ lhs)
-               $ (Const (@{const_name "Trueprop"},_) $ rhs)) = {lhs=lhs, rhs=rhs}
+               (Const (@{const_name Trueprop},_) $ lhs)
+               $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
   | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   | dest_equal tm = S.dest_eq tm;
 
@@ -759,7 +759,7 @@
               val cntxt = rev(Simplifier.prems_of_ss ss)
               val dummy = print_thms "cntxt:" cntxt
               val thy = Thm.theory_of_thm thm
-              val Const("==>",_) $ (Const(@{const_name "Trueprop"},_) $ A) $ _ = Thm.prop_of thm
+              val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
               fun genl tm = let val vlist = subtract (op aconv) globals
                                            (OldTerm.add_term_frees(tm,[]))
                             in fold_rev Forall vlist tm
diff -r 56965d8e4e11 -r f8999e19dd49 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Thu Aug 19 16:03:01 2010 +0200
@@ -483,7 +483,7 @@
      val (case_rewrites,context_congs) = extraction_thms thy
      val tych = Thry.typecheck thy
      val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
-     val Const(@{const_name "All"},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
+     val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
      val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
                    Rtype)
      val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
diff -r 56965d8e4e11 -r f8999e19dd49 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 19 12:11:57 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 19 16:03:01 2010 +0200
@@ -165,19 +165,19 @@
 
 fun mk_select (r as {Bvar,Body}) =
   let val ty = type_of Bvar
-      val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
+      val c = Const(@{const_name Eps},(ty --> HOLogic.boolT) --> ty)
   in list_comb(c,[mk_abs r])
   end;
 
 fun mk_forall (r as {Bvar,Body}) =
   let val ty = type_of Bvar
-      val c = Const(@{const_name "All"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
+      val c = Const(@{const_name All},(ty --> HOLogic.boolT) --> HOLogic.boolT)
   in list_comb(c,[mk_abs r])
   end;
 
 fun mk_exists (r as {Bvar,Body}) =
   let val ty = type_of Bvar
-      val c = Const(@{const_name "Ex"},(ty --> HOLogic.boolT) --> HOLogic.boolT)
+      val c = Const(@{const_name Ex},(ty --> HOLogic.boolT) --> HOLogic.boolT)
   in list_comb(c,[mk_abs r])
   end;
 
@@ -250,13 +250,13 @@
 fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
   | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
 
-fun dest_forall(Const(@{const_name "All"},_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
   | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
 
-fun dest_exists(Const(@{const_name "Ex"},_) $ (a as Abs _)) = fst (dest_abs [] a)
+fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a)
   | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
 
-fun dest_neg(Const("not",_) $ M) = M
+fun dest_neg(Const(@{const_name Not},_) $ M) = M
   | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
 
 fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
@@ -402,6 +402,6 @@
   | is_WFR _                 = false;
 
 fun ARB ty = mk_select{Bvar=Free("v",ty),
-                       Body=Const(@{const_name "True"},HOLogic.boolT)};
+                       Body=Const(@{const_name True},HOLogic.boolT)};
 
 end;