src/HOL/Hoare/hoare_tac.ML
changeset 37391 476270a6c2dc
parent 37138 ee23611b6bf2
child 37591 d3daea901123
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Thu Jun 10 12:24:02 2010 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Thu Jun 10 12:24:03 2010 +0200
     1.3 @@ -41,9 +41,9 @@
     1.4                 else let val (n, T) = dest_Free x ;
     1.5                          val z = mk_bodyC xs;
     1.6                          val T2 = case z of Free(_, T) => T
     1.7 -                                         | Const ("Pair", Type ("fun", [_, Type
     1.8 +                                         | Const (@{const_name Pair}, Type ("fun", [_, Type
     1.9                                              ("fun", [_, T])])) $ _ $ _ => T;
    1.10 -                 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    1.11 +                 in Const (@{const_name Pair}, [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    1.12  
    1.13  (** maps a subgoal of the form:
    1.14          VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)