--- 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"
--- 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"
--- 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