# HG changeset patch
# User obua
# Date 1154610845 -7200
# Node ID cbf31171c14709f2ea53a33ff184aef34fc17cb7
# Parent  ec52000deb44e4d0fb79bfddac37e73799195112
fixed generator

diff -r ec52000deb44 -r cbf31171c147 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Aug 03 15:03:49 2006 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Aug 03 15:14:05 2006 +0200
@@ -31,7 +31,7 @@
   TYDEF_sum
   DEF_INL
   DEF_INR
-  TYDEF_option;
+ (* TYDEF_option*);
 
 type_maps
   ind > Nat.ind
@@ -41,7 +41,7 @@
   prod > "*"
   num > nat
   sum > "+"
-  option > Datatype.option;
+(*  option > Datatype.option*);
 
 const_renames
   "==" > "eqeq"
@@ -82,8 +82,10 @@
   BIT0 > HOLLightCompat.NUMERAL_BIT0
   BIT1 > HOL4Compat.NUMERAL_BIT1
   INL > Sum_Type.Inl
-  INR > Sum_Type.Inr;
- (* HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
+  INR > Sum_Type.Inr
+ (* NONE > Datatype.None
+  SOME > Datatype.Some;
+  HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
 
 (*import_until "TYDEF_sum"
 
diff -r ec52000deb44 -r cbf31171c147 src/HOL/Import/HOL4Setup.thy
--- a/src/HOL/Import/HOL4Setup.thy	Thu Aug 03 15:03:49 2006 +0200
+++ b/src/HOL/Import/HOL4Setup.thy	Thu Aug 03 15:14:05 2006 +0200
@@ -20,7 +20,6 @@
 
 consts
   ONE_ONE :: "('a => 'b) => bool"
-  ONTO    :: "('a => 'b) => bool"
 
 defs
   ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
diff -r ec52000deb44 -r cbf31171c147 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Aug 03 15:03:49 2006 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu Aug 03 15:14:05 2006 +0200
@@ -414,13 +414,14 @@
     handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
 
 fun mk_tfree s = TFree("'"^s,[])
+fun mk_free s t = Free (s,t)
 val xT = mk_tfree "a"
 val yT = mk_tfree "b"
-val P  = Var(("P",0),xT-->yT-->propT)
-val Q  = Var(("Q",0),xT-->yT)
-val R  = Var(("R",0),xT-->yT)
-val S  = Var(("S",0),xT)
-val S'  = Var(("S'",0),xT)
+val P  = mk_free "P" (xT-->yT-->propT)
+val Q  = mk_free "Q" (xT-->yT)
+val R  = mk_free "R" (xT-->yT)
+val S  = mk_free "S" xT
+val S'  = mk_free "S'" xT
 in
 fun beta_simproc sg = Simplifier.simproc_i
 		      sg
@@ -488,23 +489,21 @@
 fun norm_term thy t =
     let
 	val sg = sign_of thy
-
 	val norms = ShuffleData.get thy
 	val ss = Simplifier.theory_context thy empty_ss
           setmksimps single
 	  addsimps (map (Thm.transfer sg) norms)
+          addsimprocs [quant_simproc sg, eta_expand_simproc sg,eta_contract_simproc sg]
 	fun chain f th =
 	    let
                 val rhs = snd (dest_equals (cprop_of th))
       	    in
 		transitive th (f rhs)
 	    end
-
 	val th =
-	    t |> disamb_bound sg
-	      |> chain (Simplifier.full_rewrite
-			    (ss addsimprocs [quant_simproc sg,eta_expand_simproc sg,eta_contract_simproc sg]))
-	      |> chain eta_conversion
+            t |> disamb_bound sg
+	      |> chain (Simplifier.full_rewrite ss)
+              |> chain eta_conversion
 	      |> strip_shyps
 	val _ = message ("norm_term: " ^ (string_of_thm th))
     in