src/HOL/Tools/Function/termination.ML
changeset 38795 848be46708dc
parent 38557 9926c47ad1a1
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4      val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
     1.5      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
     1.6        let
     1.7 -        val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
     1.8 +        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
     1.9            = Term.strip_qnt_body @{const_name Ex} c
    1.10        in cons r o cons l end
    1.11    in
    1.12 @@ -185,7 +185,7 @@
    1.13      val vs = Term.strip_qnt_vars @{const_name Ex} c
    1.14  
    1.15      (* FIXME: throw error "dest_call" for malformed terms *)
    1.16 -    val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
    1.17 +    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
    1.18        = Term.strip_qnt_body @{const_name Ex} c
    1.19      val (p, l') = dest_inj sk l
    1.20      val (q, r') = dest_inj sk r