src/FOLP/IFOLP.thy
changeset 42799 4e33894aec6d
parent 42616 92715b528e78
child 44121 44adaa6db327
     1.1 --- a/src/FOLP/IFOLP.thy	Sat May 14 00:32:16 2011 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Sat May 14 11:42:43 2011 +0200
     1.3 @@ -587,11 +587,8 @@
     1.4  use "hypsubst.ML"
     1.5  
     1.6  ML {*
     1.7 -
     1.8 -(*** Applying HypsubstFun to generate hyp_subst_tac ***)
     1.9 -
    1.10 -structure Hypsubst_Data =
    1.11 -struct
    1.12 +structure Hypsubst = Hypsubst
    1.13 +(
    1.14    (*Take apart an equality judgement; otherwise raise Match!*)
    1.15    fun dest_eq (Const (@{const_name Proof}, _) $
    1.16      (Const (@{const_name eq}, _)  $ t $ u) $ _) = (t, u);
    1.17 @@ -605,9 +602,7 @@
    1.18    val subst = @{thm subst}
    1.19    val sym = @{thm sym}
    1.20    val thin_refl = @{thm thin_refl}
    1.21 -end;
    1.22 -
    1.23 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    1.24 +);
    1.25  open Hypsubst;
    1.26  *}
    1.27