src/HOL/Import/import.ML
changeset 31945 d5f186aa0bed
parent 31723 f5cafe803b55
child 32091 30e2ffbba718
     1.1 --- a/src/HOL/Import/import.ML	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/HOL/Import/import.ML	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4                              then message "import: Terms match up"
     1.5                              else message "import: Terms DO NOT match up"
     1.6                      val thm' = equal_elim (symmetric prew) thm
     1.7 -                    val res = bicompose true (false,thm',0) 1 th
     1.8 +                    val res = Thm.bicompose true (false,thm',0) 1 th
     1.9                  in
    1.10                      res
    1.11                  end