src/HOL/Import/shuffler.ML
changeset 14518 c3019a66180f
parent 14516 a183dec876ab
child 14620 1be590fd2422
     1.1 --- a/src/HOL/Import/shuffler.ML	Fri Apr 02 17:40:32 2004 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sun Apr 04 15:34:14 2004 +0200
     1.3 @@ -263,7 +263,8 @@
     1.4  		  (([],tfree_names),tvars)
     1.5  	val t' = subst_TVars type_inst t
     1.6      in
     1.7 -	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))) type_inst)
     1.8 +	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
     1.9 +		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
    1.10      end
    1.11  
    1.12  fun inst_tfrees sg [] thm = thm