src/HOL/Import/import_syntax.ML
changeset 17644 bd59bfd4bf37
parent 17370 754b7fcff03e
child 19064 bf19cc5a7899
     1.1 --- a/src/HOL/Import/import_syntax.ML	Mon Sep 26 02:06:44 2005 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Mon Sep 26 02:27:14 2005 +0200
     1.3 @@ -50,6 +50,8 @@
     1.4  		val segname = get_import_segment thy
     1.5  		val (int_thms,facts) = Replay.setup_int_thms thyname thy
     1.6  		val thmnames = List.filter (not o should_ignore thyname thy) facts
     1.7 +               (* val _ = set show_types
     1.8 +                val _ = set show_sorts*)
     1.9  	    in
    1.10  		thy |> clear_import_thy
    1.11  		    |> set_segment thyname segname