src/HOL/Library/reflection.ML
changeset 37117 59cee8807c29
parent 36945 9bec62c10714
child 38549 d0385f2764d8
     1.1 --- a/src/HOL/Library/reflection.ML	Tue May 25 20:22:55 2010 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Tue May 25 20:28:16 2010 +0200
     1.3 @@ -140,24 +140,25 @@
     1.4                     bds)
     1.5                 end)
     1.6             | _ => da (s,ctxt) bds)
     1.7 -      in (case cgns of
     1.8 +      in
     1.9 +        (case cgns of
    1.10            [] => tryabsdecomp (t,ctxt) bds
    1.11 -        | ((vns,cong)::congs) => ((let
    1.12 -            val cert = cterm_of thy
    1.13 -            val certy = ctyp_of thy
    1.14 -            val (tyenv, tmenv) =
    1.15 -              Pattern.match thy
    1.16 -                ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
    1.17 -                (Vartab.empty, Vartab.empty)
    1.18 -            val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv)
    1.19 -            val (fts,its) =
    1.20 -              (map (snd o snd) fnvs,
    1.21 -               map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    1.22 -            val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
    1.23 -          in ((fts ~~ (replicate (length fts) ctxt),
    1.24 -               Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
    1.25 -          end)
    1.26 -        handle MATCH => decomp_genreif da congs (t,ctxt) bds))
    1.27 +        | ((vns,cong)::congs) =>
    1.28 +            (let
    1.29 +              val cert = cterm_of thy
    1.30 +              val certy = ctyp_of thy
    1.31 +              val (tyenv, tmenv) =
    1.32 +                Pattern.match thy
    1.33 +                  ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
    1.34 +                  (Vartab.empty, Vartab.empty)
    1.35 +              val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv)
    1.36 +              val (fts,its) =
    1.37 +                (map (snd o snd) fnvs,
    1.38 +                 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
    1.39 +              val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
    1.40 +            in ((fts ~~ (replicate (length fts) ctxt),
    1.41 +                 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
    1.42 +            end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
    1.43        end;
    1.44  
    1.45   (* looks for the atoms equation and instantiates it with the right number *)
    1.46 @@ -231,7 +232,7 @@
    1.47                in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts)  end
    1.48              val th = (instantiate (subst_ty, substt)  eq) RS sym
    1.49            in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
    1.50 -          handle MATCH => tryeqs eqs bds)
    1.51 +          handle Pattern.MATCH => tryeqs eqs bds)
    1.52        in tryeqs (filter isat eqs) bds end), bds);
    1.53  
    1.54    (* Generic reification procedure: *)