--- a/src/HOL/Tools/Function/termination.ML Thu Aug 19 16:08:53 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Aug 19 16:08:54 2010 +0200
@@ -149,7 +149,7 @@
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
- = Term.strip_qnt_body "Ex" c
+ = Term.strip_qnt_body @{const_name Ex} c
in cons r o cons l end
in
mk_skel (fold collect_pats cs [])
@@ -182,11 +182,11 @@
fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
val (sk, _, _, _, _) = D
- val vs = Term.strip_qnt_vars "Ex" c
+ val vs = Term.strip_qnt_vars @{const_name Ex} c
(* FIXME: throw error "dest_call" for malformed terms *)
val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
- = Term.strip_qnt_body "Ex" c
+ = Term.strip_qnt_body @{const_name Ex} c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
in