src/HOL/Import/shuffler.ML
changeset 36614 b6c031ad3690
parent 36543 0e7fc5bf38de
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Import/shuffler.ML	Mon May 03 15:34:55 2010 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Mon May 03 16:26:47 2010 +0200
     1.3 @@ -502,7 +502,7 @@
     1.4              t |> disamb_bound thy
     1.5                |> chain (Simplifier.full_rewrite ss)
     1.6                |> chain eta_conversion
     1.7 -              |> strip_shyps
     1.8 +              |> Thm.strip_shyps
     1.9          val _ = message ("norm_term: " ^ (string_of_thm th))
    1.10      in
    1.11          th