prefer internal types, via Simple_Syntax.read_typ;
authorwenzelm
Tue Apr 19 21:33:56 2011 +0200 (2011-04-19)
changeset 424075b9dd52f5dca
parent 42406 05f2468d6b36
child 42408 282b7a3065d3
prefer internal types, via Simple_Syntax.read_typ;
src/Pure/Proof/extraction.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Apr 19 21:19:14 2011 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Apr 19 21:33:56 2011 +0200
     1.3 @@ -32,16 +32,17 @@
     1.4  
     1.5  (**** tools ****)
     1.6  
     1.7 -fun add_syntax thy =
     1.8 -  thy
     1.9 -  |> Theory.copy
    1.10 -  |> Sign.root_path
    1.11 -  |> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
    1.12 -  |> Sign.add_consts
    1.13 -      [(Binding.name "typeof", "'b::{} => Type", NoSyn),
    1.14 -       (Binding.name "Type", "'a::{} itself => Type", NoSyn),
    1.15 -       (Binding.name "Null", "Null", NoSyn),
    1.16 -       (Binding.name "realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
    1.17 +val typ = Simple_Syntax.read_typ;
    1.18 +
    1.19 +val add_syntax =
    1.20 +  Theory.copy
    1.21 +  #> Sign.root_path
    1.22 +  #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
    1.23 +  #> Sign.add_consts_i
    1.24 +      [(Binding.name "typeof", typ "'b => Type", NoSyn),
    1.25 +       (Binding.name "Type", typ "'a itself => Type", NoSyn),
    1.26 +       (Binding.name "Null", typ "Null", NoSyn),
    1.27 +       (Binding.name "realizes", typ "'a => 'b => 'b", NoSyn)];
    1.28  
    1.29  val nullT = Type ("Null", []);
    1.30  val nullt = Const ("Null", nullT);
    1.31 @@ -530,7 +531,7 @@
    1.32        | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
    1.33            let
    1.34              val T = etype_of thy' vs Ts prop;
    1.35 -            val u = if T = nullT then 
    1.36 +            val u = if T = nullT then
    1.37                  (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
    1.38                else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
    1.39              val (defs', corr_prf) =