src/HOL/Tools/specification_package.ML
changeset 15794 5de27a5fc5ed
parent 15574 b1d1b5bfc464
child 15945 08e8d3fb9343
equal deleted inserted replaced
15793:acfdd493f5c4 15794:5de27a5fc5ed
   108     let
   108     let
   109 	val fmap' = map Library.swap fmap
   109 	val fmap' = map Library.swap fmap
   110 	fun unthaw (f as (a,S)) =
   110 	fun unthaw (f as (a,S)) =
   111 	    (case assoc (fmap',a) of
   111 	    (case assoc (fmap',a) of
   112 		 NONE => TVar f
   112 		 NONE => TVar f
   113 	       | SOME b => TFree (b,S))
   113 	       | SOME (b, _) => TFree (b,S))
   114     in
   114     in
   115 	map_term_types (map_type_tvar unthaw) t
   115 	map_term_types (map_type_tvar unthaw) t
   116     end
   116     end
   117 
   117 
   118 (* The syntactic meddling needed to setup add_specification for work *)
   118 (* The syntactic meddling needed to setup add_specification for work *)