src/HOL/Import/shuffler.ML
changeset 14854 61bdf2ae4dc5
parent 14848 83f1dc18f1f1
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Jun 01 11:25:26 2004 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Jun 01 12:33:50 2004 +0200
     1.3 @@ -132,8 +132,8 @@
     1.4  val def_norm =
     1.5      let
     1.6  	val cert = cterm_of (sign_of ProtoPure.thy)
     1.7 -	val aT = TFree("'a",logicS)
     1.8 -	val bT = TFree("'b",logicS)
     1.9 +	val aT = TFree("'a",[])
    1.10 +	val bT = TFree("'b",[])
    1.11  	val v = Free("v",aT)
    1.12  	val P = Free("P",aT-->bT)
    1.13  	val Q = Free("Q",aT-->bT)
    1.14 @@ -159,8 +159,8 @@
    1.15  val all_comm =
    1.16      let
    1.17  	val cert = cterm_of (sign_of ProtoPure.thy)
    1.18 -	val xT = TFree("'a",logicS)
    1.19 -	val yT = TFree("'b",logicS)
    1.20 +	val xT = TFree("'a",[])
    1.21 +	val yT = TFree("'b",[])
    1.22  	val P = Free("P",xT-->yT-->propT)
    1.23  	val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
    1.24  	val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
    1.25 @@ -404,7 +404,7 @@
    1.26      end
    1.27      handle e => (writeln "eta_expand internal error";print_exn e)
    1.28  
    1.29 -fun mk_tfree s = TFree("'"^s,logicS)
    1.30 +fun mk_tfree s = TFree("'"^s,[])
    1.31  val xT = mk_tfree "a"
    1.32  val yT = mk_tfree "b"
    1.33  val P  = Var(("P",0),xT-->yT-->propT)
    1.34 @@ -495,8 +495,6 @@
    1.35      end
    1.36      handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
    1.37  
    1.38 -fun is_logic_var sg v =
    1.39 -    Type.of_sort (Sign.tsig_of sg) (type_of v,logicS)
    1.40  
    1.41  (* Closes a theorem with respect to free and schematic variables (does
    1.42  not touch type variables, though). *)
    1.43 @@ -505,10 +503,9 @@
    1.44      let
    1.45  	val sg = sign_of_thm th
    1.46  	val c = prop_of th
    1.47 -	val all_vars = add_term_frees (c,add_term_vars(c,[]))
    1.48 -	val all_rel_vars = filter (is_logic_var sg) all_vars
    1.49 +	val vars = add_term_frees (c,add_term_vars(c,[]))
    1.50      in
    1.51 -	Drule.forall_intr_list (map (cterm_of sg) all_rel_vars) th
    1.52 +	Drule.forall_intr_list (map (cterm_of sg) vars) th
    1.53      end
    1.54      handle e => (writeln "close_thm internal error"; print_exn e)
    1.55  
    1.56 @@ -572,10 +569,9 @@
    1.57  fun set_prop thy t =
    1.58      let
    1.59  	val sg = sign_of thy
    1.60 -	val all_vars = add_term_frees (t,add_term_vars (t,[]))
    1.61 -	val all_rel_vars = filter (is_logic_var sg) all_vars
    1.62 +	val vars = add_term_frees (t,add_term_vars (t,[]))
    1.63  	val closed_t = foldr (fn (v,body) => let val vT = type_of v
    1.64 -					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (all_rel_vars,t)
    1.65 +					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t)
    1.66  	val rew_th = norm_term thy closed_t
    1.67  	val rhs = snd (dest_equals (cprop_of rew_th))
    1.68  
    1.69 @@ -596,7 +592,7 @@
    1.70  			val closed_th = equal_elim (symmetric rew_th) mod_th
    1.71  		    in
    1.72  			message ("Shuffler.set_prop succeeded by " ^ name);
    1.73 -			Some (name,forall_elim_list (map (cterm_of sg) all_rel_vars) closed_th)
    1.74 +			Some (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
    1.75  		    end
    1.76  		  | None => process thms
    1.77  	    end